Frama-C Bug Tracking System - Frama-C
View Issue Details
0002292Frama-CPlug-in > wppublic2017-03-13 17:572017-03-16 11:10
Frama-C 14-Silicon 
0002292: signature axiom omitted in Coq and Alt-ergo translation
Running "frama-c -wp -wp-prover cvc4 -wp-prover alt-ergo -wp-prover coq -wp-script wp0.script -wp-prop incAdd input_it.c" on the attached file generates an insufficient translation to Coq: There is a clause "Parameter L_add : S1__Iter -> Z -> S1__Iter." in file "lemma_incAdd_Coq.v", but no corresponding "Hypothesis Q_TL_add". Both clauses are needed to describe the signature of the Acsl logic function "add". The hypothesis "Q_TL_add" would be needed in the Coq proof (see out-commented lines in file "wp0.script"). For the Acsl function "inc", which is defined in a different "axiomatic" block, both signature description clauses (viz. "Parameter L_inc" and "Hypothesis Q_TL_inc") are contained in file "A_IterAxioms.v". When considering the output to Alt-Ergo, viz. file "lemma_incAdd_Alt-Ergo.mlw", the same problem appears: there is a declaration "logic L_inc" in line 606, an "axiom Q_TL_inc" in line 610, a declaration "logic L_add" in line 632, but no corresponding "axiom Q_TL_add". When considering the output to Why3, everything appears to be ok: in file "A_addAxioms.why", both "function l_add" and "axiom Q_TL_add" is found, and in file "A_IterAxioms.why", both "function l_inc" and "axiom Q_TL_inc" is found.
No tags attached.
c input_it.c (633) 2017-03-13 17:57
? wp0.script (340) 2017-03-13 17:58
? lemma_incAdd_Coq.v (1,086) 2017-03-13 17:58
? A_IterAxioms.v (1,093) 2017-03-13 17:59
? lemma_incAdd_Alt-Ergo.mlw (25,297) 2017-03-13 17:59
? A_addAxioms.why (1,056) 2017-03-13 18:00
? A_IterAxioms.why (927) 2017-03-13 18:00
Issue History
2017-03-13 17:57JochenNew Issue
2017-03-13 17:57JochenStatusnew => assigned
2017-03-13 17:57JochenAssigned To => correnson
2017-03-13 17:57JochenFile Added: input_it.c
2017-03-13 17:58JochenFile Added: wp0.script
2017-03-13 17:58JochenFile Added: lemma_incAdd_Coq.v
2017-03-13 17:59JochenFile Added: A_IterAxioms.v
2017-03-13 17:59JochenFile Added: lemma_incAdd_Alt-Ergo.mlw
2017-03-13 18:00JochenFile Added: A_addAxioms.why
2017-03-13 18:00JochenFile Added: A_IterAxioms.why
2017-03-16 11:10jensNote Added: 0006388

2017-03-16 11:10   
From my point of view it is not a "minor" issue because it really impedes the discharge of some proof obligations with Coq.