obligation "2+2==5" simplified to "false" by Qed, but then passed to Alt-Ergo nevertheless
ID0001999: This issue was created automatically from Mantis Issue 1999. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001999 | Frama-Clang | Plug-in > wp | public | 2014-11-27 | 2014-11-27 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | frama-c-Neon-20140301+dev-stance | OS | - | OS Version | xubuntu-cfe13.10 |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp 167.c" on the attached program yields the output:
... [wp] [Alt-Ergo] Goal typed_foo_assert : Unknown ...
The corresponding file "foo_assert_Alt-Ergo.mlw" contains the goal "goal foo_assert: false", in line 369.
Apparently, Qed succeeds to recognize that the assertion in line 3 of file "167.c" is provably wrong. However, the obligation is passed to the external prover Alt-Ergo nevertheless.
Similar to goals recognized as true by Qed, goals recognized as false needn't be passed to subsequent provers.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information