signature axiom omitted in Coq and Alt-ergo translation
ID0002292: This issue was created automatically from Mantis Issue 2292. Further discussion may take place here.
|ID0002292||Frama-C||Plug-in > wp||public||2017-03-13||2017-03-16|
|Product Version||Frama-C 14-Silicon||Target Version||-||Fixed in Version||-|
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.