Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000456Frama-CPlug-in > jessiepublic2010-04-23 12:212010-04-23 12:21
Reportergava 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000456: Lack of parameter generation
DescriptionThe following program (even if there are not enought annotations) works with Frama-C Berylium (with why-2.23) but crashes with Boron/why-2.24 The VC of WHY is launched and it said that a parameter is missing... The pb does not arise with why-2.23/Brylium Frédéric G. ps: the file "bsp.h" in the "additional information" pps : I used "frama-c -jessie bspinprod.c"
Additional Informationtypedef value_type; /*@ axiomatic GoodNumberProcessor { logic integer bsp_p; axiom good_bsp_p: 0
TagsNo tags attached.
Attached Filesc file icon bspinprod.c [^] (3,355 bytes) 2010-04-23 12:21 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-04-23 12:21 gava New Issue
2010-04-23 12:21 gava Status new => assigned
2010-04-23 12:21 gava Assigned To => cmarche
2010-04-23 12:21 gava File Added: bspinprod.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker