Frama-C Bug Tracking System - Frama-C
View Issue Details
0000456Frama-CPlug-in > jessiepublic2010-04-23 12:212010-04-23 12:21
gava 
cmarche 
normalminoralways
assignedopen 
Frama-C Boron-20100401 
 
0000456: Lack of parameter generation
The 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"
typedef value_type; /*@ axiomatic GoodNumberProcessor { logic integer bsp_p; axiom good_bsp_p: 0
No tags attached.
c bspinprod.c (3,355) 2010-04-23 12:21
https://bts.frama-c.com/file_download.php?file_id=78&type=bug
Issue History
2010-04-23 12:21gavaNew Issue
2010-04-23 12:21gavaStatusnew => assigned
2010-04-23 12:21gavaAssigned To => cmarche
2010-04-23 12:21gavaFile Added: bspinprod.c

There are no notes attached to this issue.