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.
|ID0002169||Frama-C||Plug-in > wp||public||2015-09-21||2015-09-21|
|Product Version||-||Target Version||-||Fixed in Version||-|
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".
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information