Frama-C Bug Tracking System - Frama-C
View Issue Details
0000024Frama-CPlug-in > jessiepublic2009-04-07 13:552011-10-28 10:39
virgile 
cmarche 
normalminoralways
closedfixed 
Frama-C Lithium-20081201 
Frama-C Nitrogen-20111001 
0000024: Ordering of lemma in coq output of jessie
(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.
No tags attached.
c logic.c (129) 2009-04-07 13:55
https://bts.frama-c.com/file_download.php?file_id=2&type=bug
Issue History
2009-04-07 13:55virgileNew Issue
2009-04-07 13:55virgileFile Added: logic.c
2009-04-07 15:43signolesStatusnew => acknowledged
2009-04-07 16:05signolesStatusacknowledged => assigned
2009-04-07 16:05signolesAssigned To => monate
2009-04-07 18:00monateAssigned Tomonate =>
2009-04-07 18:15signolesStatusassigned => acknowledged
2009-04-10 10:03signolesStatusacknowledged => assigned
2009-04-10 10:03signolesAssigned To => cmarche
2011-03-11 11:20cmarcheNote Added: 0001593
2011-03-11 11:20cmarcheResolutionopen => fixed
2011-04-01 15:22cmarcheStatusassigned => resolved
2011-10-10 14:14signolesStatusresolved => closed
2011-10-10 14:15signolesStatusclosed => resolved
2011-10-28 10:39signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-28 10:39signolesStatusresolved => closed

Notes
(0001593)
cmarche   
2011-03-11 11:20   
This will be fixed in Why 2.30