Frama-C Bug Tracking System - Frama-C
View Issue Details
0001586Frama-CPlug-in > wppublic2013-12-16 11:102014-03-13 15:57
correnson 
correnson 
normalmajorhave not tried
closedfixed 
 
Frama-C Neon-20140301 
0001586: Bug in let-elimination (due to <==> and assert false).
Bug in let-elimination (due to <==> and assert false). Using -wp-no-let makes the assert false not-proved as expected.
In 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.
No tags attached.
c q19_switch_fun_call.c (1,335) 2013-12-16 11:10
https://bts.frama-c.com/file_download.php?file_id=621&type=bug
c q20_switch_fun_call.c (1,276) 2013-12-16 11:45
https://bts.frama-c.com/file_download.php?file_id=622&type=bug
Issue History
2013-12-16 11:10corrensonNew Issue
2013-12-16 11:10corrensonStatusnew => assigned
2013-12-16 11:10corrensonAssigned To => correnson
2013-12-16 11:10corrensonFile Added: q19_switch_fun_call.c
2013-12-16 11:45dmentreFile Added: q20_switch_fun_call.c
2013-12-16 11:46dmentreNote Added: 0004377
2014-02-05 16:29corrensonNote Added: 0004505
2014-02-05 16:29corrensonStatusassigned => resolved
2014-02-05 16:29corrensonResolutionopen => fixed
2014-02-12 16:57corrensonNote Added: 0004533
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed

Notes
(0004377)
dmentre   
2013-12-16 11:46   
Another example added. VC for "assert x > 0;" has False in hypothesis.
(0004505)
correnson   
2014-02-05 16:29   
Fix committed to master branch.
(0004533)
correnson   
2014-02-12 16:57   
Fix committed to stable/neon branch.