same formula translated differently as axiom/lemma
ID0000420: This issue was created automatically from Mantis Issue 420. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000420 | Frama-C | Plug-in > jessie | public | 2010-02-25 | 2010-04-19 |
| Reporter | Jochen | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Beryllium-20090902 | Target Version | - | Fixed in Version | Frama-C Boron-20100401 |
Description :
Axiom ax2 (line 5,6 in attached file) is translated into a proof obligation on 2 memory labels. However, in lemma lm1 (line 11,12), the literally same formula is translated into a proof obligation on 4 memory labels; and so is the assertion in line 24, which is an instance of the ax2/lm1 formula.
As a consequence, when lm1 is omitted, the assertion cannot be proved (by Alt-ergo; Simplify doesnt prove it in any case); but when lm1 is present, the assertion can be proved, while the lemma itself can not.
(While the example program in the attached file is nonsensical, it has been boiled down from a program that does make sense.)