Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000420Frama-CPlug-in > jessiepublic2010-02-25 21:172010-04-19 16:14
Assigned Tocmarche 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000420: same formula translated differently as axiom/lemma
DescriptionAxiom 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.)
TagsNo tags attached.
Attached Filesc file icon axiomLabels01.c [^] (701 bytes) 2010-02-25 21:17 [Show Content]

- Relationships

-  Notes
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).

- Issue History
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

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker