insertion of "assert true" after a statement influences provability of the statement's contract
ID0002226: This issue was created automatically from Mantis Issue 2226. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002226 | Frama-C | Kernel | public | 2016-05-02 | 2016-05-04 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Sodium-20150201 | OS | xubuntu14.04 | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp p1on.c" on the attached program proves both the statement contract in line 9 and the trivial assertion in line 11, as expected.
However, if line 11 is commented out, Alt-Ergo immediately reports "unknown" on line 9. (Cvc4 runs into its timeout then.) The file "foo_stmt_post_Alt-Ergo.mlw" contains the goal "goal foo_stmt_post: false" for some reason.
It seems that the statement contract is translated in a wrong way, unless the final trivla assertion is present in line 11.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information