View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000420 | Frama-C | Plug-in > jessie | public | 2010-02-25 21:17 | 2010-04-19 16:14 | ||||
Reporter | Jochen | ||||||||
Assigned To | cmarche | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Beryllium-20090902 | ||||||||
Target Version | Fixed in Version | Frama-C Boron-20100401 | |||||||
Summary | 0000420: same formula translated differently as axiom/lemma | ||||||||
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.) | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
cmarche (developer) 2010-03-30 17:53 |
Fixed a bug in computation of read effects |
signoles (manager) 2010-04-19 16:14 |
Fix in Why 2.24 (require Frama-C Boron-20100401). |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2010-02-25 21:17 | Jochen | New Issue | |
2010-02-25 21:17 | Jochen | Status | new => assigned |
2010-02-25 21:17 | Jochen | Assigned To | => cmarche |
2010-02-25 21:17 | Jochen | File Added: axiomLabels01.c | |
2010-03-30 17:53 | cmarche | Note Added: 0000747 | |
2010-03-30 17:53 | cmarche | Status | assigned => resolved |
2010-03-30 17:53 | cmarche | Resolution | open => fixed |
2010-04-19 16:13 | signoles | Status | resolved => closed |
2010-04-19 16:13 | signoles | Fixed in Version | => Frama-C Boron |
2010-04-19 16:14 | signoles | Note Added: 0000775 |