Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001586Frama-CPlug-in > wppublic2013-12-16 11:102014-03-13 15:57
Reportercorrenson 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001586: Bug in let-elimination (due to <==> and assert false).
DescriptionBug in let-elimination (due to <==> and assert false).
Using -wp-no-let makes the assert false not-proved as expected.
Additional InformationIn the attached program, we have no assumption and everything is proved
with WP (Frama-C Fluorine June), including the assert 1==2 in case N!

   frama-c-gui -pp-annot -wp -wp-rte q19_switch_fun_call.c

It appears that the issue is coming from the equivalences used in the
behaviours of compute_trans(). If we replace "<==>" by "==>", then the
1==2 assert is not proved (substitute call to compute_trans() by
compute_trans2() in main()).

In both cases (compute_trans() and compute_trans2()), the contract is
always proved.
TagsNo tags attached.
Attached Filesc file icon q19_switch_fun_call.c [^] (1,335 bytes) 2013-12-16 11:10 [Show Content]
c file icon q20_switch_fun_call.c [^] (1,276 bytes) 2013-12-16 11:45 [Show Content]

- Relationships

-  Notes
(0004377)
dmentre (reporter)
2013-12-16 11:46

Another example added. VC for "assert x > 0;" has False in hypothesis.
(0004505)
correnson (manager)
2014-02-05 16:29

Fix committed to master branch.
(0004533)
correnson (manager)
2014-02-12 16:57

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2013-12-16 11:10 correnson New Issue
2013-12-16 11:10 correnson Status new => assigned
2013-12-16 11:10 correnson Assigned To => correnson
2013-12-16 11:10 correnson File Added: q19_switch_fun_call.c
2013-12-16 11:45 dmentre File Added: q20_switch_fun_call.c
2013-12-16 11:46 dmentre Note Added: 0004377
2014-02-05 16:29 correnson Note Added: 0004505
2014-02-05 16:29 correnson Status assigned => resolved
2014-02-05 16:29 correnson Resolution open => fixed
2014-02-12 16:57 correnson Note Added: 0004533
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker