naming the default behavior influences proven obligations
ID0002309: This issue was created automatically from Mantis Issue 2309. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002309 | Frama-C | Plug-in > wp | public | 2017-06-01 | 2017-06-01 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Phosphorus-20170501-beta1 | OS | xubuntu | OS Version | - |
| Product Version | Frama-C 15-Phosphorus | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp ilog2_beh.c -wp-prop ilog2 -wp-prover alt-ergo -wp-prover cvc4" on the attached program proves everything except (the lemmas and) loop invariant "a".
However, when lines 16,27,30,36,41 are uncommented, i.e. the default behavior is assigned an explicit name, everything except (the lemmas and) the loop variant is proven instead.
Naming vs. not naming a behavior shouldn't have such an influence.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information