suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"
ID0002336: This issue was created automatically from Mantis Issue 2336. Further discussion may take place here.
|ID0002336||Frama-C||Plug-in > wp||public||2017-12-08||2019-10-17|
|Platform||Sulfur-20171101||OS||-||OS Version||Ubuntu 17.04|
|Product Version||-||Target Version||-||Fixed in Version||-|
Running "frama-c -wp -wp-rte foo.c -wp-out wp-out" on the attached file fails to prove clauses "E1" (as expected) and "E2". The latter is provable from "E1" by axiom "a2". A look at file "main_post_E2_Alt-Ergo.mlw" reveals that "E1" isn't given as hypothesis, and hence axiom "a2" can't be applied.
I cannot judge whether there is good reason for this behavior of Frama-C/Wp. If there isn't, I suggest that "E1" should be given as hypothesis to the proof obligation for "E2", similar to Frama-C/Wp's behavior on consecutive "assigns" clauses. The same applies to statement contracts.