Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002292Frama-CPlug-in > wppublic2017-03-13 17:572017-03-16 11:10
Assigned Tocorrenson 
PlatformSilicon-20161101OSxubuntuOS Version
Product VersionFrama-C Silicon 
Target VersionFixed in Version 
Summary0002292: signature axiom omitted in Coq and Alt-ergo translation
DescriptionRunning "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.
TagsNo tags attached.
Attached Filesc file icon input_it.c [^] (633 bytes) 2017-03-13 17:57 [Show Content]
? file icon wp0.script [^] (340 bytes) 2017-03-13 17:58
? file icon lemma_incAdd_Coq.v [^] (1,086 bytes) 2017-03-13 17:58
? file icon A_IterAxioms.v [^] (1,093 bytes) 2017-03-13 17:59
? file icon lemma_incAdd_Alt-Ergo.mlw [^] (25,297 bytes) 2017-03-13 17:59
? file icon A_addAxioms.why [^] (1,056 bytes) 2017-03-13 18:00
? file icon A_IterAxioms.why [^] (927 bytes) 2017-03-13 18:00

- Relationships

-  Notes
jens (reporter)
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.

- Issue History
Date Modified Username Field Change
2017-03-13 17:57 Jochen New Issue
2017-03-13 17:57 Jochen Status new => assigned
2017-03-13 17:57 Jochen Assigned To => correnson
2017-03-13 17:57 Jochen File Added: input_it.c
2017-03-13 17:58 Jochen File Added: wp0.script
2017-03-13 17:58 Jochen File Added: lemma_incAdd_Coq.v
2017-03-13 17:59 Jochen File Added: A_IterAxioms.v
2017-03-13 17:59 Jochen File Added: lemma_incAdd_Alt-Ergo.mlw
2017-03-13 18:00 Jochen File Added: A_addAxioms.why
2017-03-13 18:00 Jochen File Added: A_IterAxioms.why
2017-03-16 11:10 jens Note Added: 0006388

Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker