incomplete Alt-Ergo obligation files generated in presence of lemma "forall int x; ..." with "x" not occurring in "..."
ID0002169: This issue was created automatically from Mantis Issue 2169. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002169 | Frama-C | Plug-in > wp | public | 2015-09-21 | 2015-09-21 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Sodium-20150201 | OS | - | OS Version | xubuntu14.04 |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp 483.c -wp-out wp-out" on the attached file generates an Alt-Ergo obligation file "foo_assert_Alt-Ergo.mlw" which contains neither the lemma "xxx" nor the proof goal for the assertion in line 5. Apparently, Frama-C/Wp tacitly crashes during translating the lemma.
The problem disappears ifin line 2 "int" is changed to "integer", or "\false" is changed to some formula containing "x".