Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000024Frama-CPlug-in > jessiepublic2009-04-07 13:552011-10-28 10:39
Reportervirgile 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000024: Ordering of lemma in coq output of jessie
Description(bug 5878 from old bts)
The file in attachment declares a predicate together with two axioms on it, and has a lemma which can be inferred from
the axioms. However, in the coq output, axioms and lemmas are sorted alphabetically, so that the lemma comes before
the axioms, making the proof impossible to complete. The relative ordering of axioms and lemmas in the C file should
be preserved.
TagsNo tags attached.
Attached Filesc file icon logic.c [^] (129 bytes) 2009-04-07 13:55 [Show Content]

- Relationships

-  Notes
(0001593)
cmarche (developer)
2011-03-11 11:20


This will be fixed in Why 2.30

- Issue History
Date Modified Username Field Change
2009-04-07 13:55 virgile New Issue
2009-04-07 13:55 virgile File Added: logic.c
2009-04-07 15:43 signoles Status new => acknowledged
2009-04-07 16:05 signoles Status acknowledged => assigned
2009-04-07 16:05 signoles Assigned To => monate
2009-04-07 18:00 monate Assigned To monate =>
2009-04-07 18:15 signoles Status assigned => acknowledged
2009-04-10 10:03 signoles Status acknowledged => assigned
2009-04-10 10:03 signoles Assigned To => cmarche
2011-03-11 11:20 cmarche Note Added: 0001593
2011-03-11 11:20 cmarche Resolution open => fixed
2011-04-01 15:22 cmarche Status assigned => resolved
2011-10-10 14:14 signoles Status resolved => closed
2011-10-10 14:15 signoles Status closed => resolved
2011-10-28 10:39 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-28 10:39 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker