2021-02-27 11:19 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000024Frama-CPlug-in > jessiepublic2011-10-28 10:39
Reportervirgile 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon logic.c (129 bytes) 2009-04-07 13:55 -
    /*@ predicate foo(integer x) reads x; */
    
    /*@ axiom f0: foo(0); */
    
    /*@ axiom f1: foo(1); */
    
    /*@ lemma e0: foo(0) && foo(1); */
    
    c file icon logic.c (129 bytes) 2009-04-07 13:55 +

-Relationships
+Relationships

-Notes

~0001593

cmarche (developer)


This will be fixed in Why 2.30
+Notes

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