ID0002336: **This issue was created automatically from Mantis Issue 2336. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002336 | Frama-C | Plug-in > wp | public | 2017-12-08 | 2019-10-17 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | suspended | | **Priority** | normal | **Severity** | tweak | **Reproducibility** | always | | **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.04 | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | - | ### Description : 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. ## Attachments - [foo.c](/uploads/5ad3994f41ed8b1f3aec521fbbf78ded/foo.c)