Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002291Frama-CPlug-in > wppublic2017-03-13 16:262017-03-13 16:33
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformSilicon-20161101OSxubuntuOS Version
Product VersionFrama-C Silicon 
Target VersionFixed in Version 
Summary0002291: suggestion: translate axioms and implication premises in forward order to coq
DescriptionRunning "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.
TagsNo tags attached.
Attached Filesc file icon coqtest.c [^] (343 bytes) 2017-03-13 16:26 [Show Content]
? file icon A_eqAxioms.v [^] (706 bytes) 2017-03-13 16:27
? file icon lemma_goal_Coq.v [^] (740 bytes) 2017-03-13 16:27

- Relationships

-  Notes
(0006383)
jens (reporter)
2017-03-13 16:33

Regarding the naming of locally bound variables, this has already been reported in https://bts.frama-c.com/view.php?id=1630 [^]

- Issue History
Date Modified Username Field Change
2017-03-13 16:26 Jochen New Issue
2017-03-13 16:26 Jochen Status new => assigned
2017-03-13 16:26 Jochen Assigned To => correnson
2017-03-13 16:26 Jochen File Added: coqtest.c
2017-03-13 16:27 Jochen File Added: A_eqAxioms.v
2017-03-13 16:27 Jochen File Added: lemma_goal_Coq.v
2017-03-13 16:33 jens Note Added: 0006383


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker