assertion not proved anymore by WP
ID0001941: This issue was created automatically from Mantis Issue 1941. Further discussion may take place here.
|ID0001941||Frama-C||Plug-in > wp||public||2014-10-23||2014-12-16|
|Reporter||Anne||Assigned To||correnson||Resolution||no change required|
|Priority||normal||Severity||minor||Reproducibility||have not tried|
|Product Version||Frama-C Neon-20140301||Target Version||-||Fixed in Version||-|
In a program similar to the enclosed example, the e1_wp property was proved by a previous version of WP, but is not proved anymore with Neon. Adding the commented loop invariant doesn't help. I tried to simplify as much as I can, but I don't understand what is going wrong in the proof obligation.
Steps To Reproduce :
$ frama-c -wp-prop a1_val bts1940.c