Bug in let-elimination (due to <==> and assert false).
ID0001586: This issue was created automatically from Mantis Issue 1586. Further discussion may take place here.
|ID0001586||Frama-C||Plug-in > wp||public||2013-12-16||2014-03-13|
|Priority||normal||Severity||major||Reproducibility||have not tried|
|Product Version||-||Target Version||-||Fixed in Version||Frama-C Neon-20140301|
Bug in let-elimination (due to <==> and assert false). Using -wp-no-let makes the assert false not-proved as expected.
Additional Information :
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.