Frama-C Bug Tracking System - Frama-C
View Issue Details
0002291Frama-CPlug-in > wppublic2017-03-13 16:262017-03-13 16:33
Frama-C 14-Silicon 
0002291: suggestion: translate axioms and implication premises in forward order to coq
Running "frama-c -wp -wp-prover coq -wp-out wp-out coqtest.c" on the attached file generates two Coq files, viz. "A_eqAxioms.v" and "lemma_goal_Coq.v". The former contains the translation of "axiomatic eqAxioms", with the axioms ("eqRefl" and "eqTrns") appearing in the same order as in the source. The file "lemma_goal_Coq.v" contains the translation of "axiomatic incAxioms", however, with the axioms ("incLf" and "incRg") appearing in reverse order, compared to the source. A similar issue concerns the translation of the body formula of axiom "eqTrns", where the first and second premise, viz. "eq(x,y)" and "eq(y,z)" in the source, appear in reverse order in the Coq translation. (As a side remark: names of locally bound variables could be translated such that a target name closely resembles its source name; for example the source name could appear as a prefix of the target name.) While probably easy to implement, these suggestions would considerably lower the overall complexity of the user's task.
No tags attached.
c coqtest.c (343) 2017-03-13 16:26
? A_eqAxioms.v (706) 2017-03-13 16:27
? lemma_goal_Coq.v (740) 2017-03-13 16:27
Issue History
2017-03-13 16:26JochenNew Issue
2017-03-13 16:26JochenStatusnew => assigned
2017-03-13 16:26JochenAssigned To => correnson
2017-03-13 16:26JochenFile Added: coqtest.c
2017-03-13 16:27JochenFile Added: A_eqAxioms.v
2017-03-13 16:27JochenFile Added: lemma_goal_Coq.v
2017-03-13 16:33jensNote Added: 0006383

2017-03-13 16:33   
Regarding the naming of locally bound variables, this has already been reported in