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.
| 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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information