Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002100Frama-CPlug-in > wppublic2015-03-31 17:152019-10-17 18:03
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionwon't fix 
PlatformOSOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002100: readability of coq(?) names
DescriptionConsider the following ACSL lemma: /*@ lemma X : \forall integer a, b; (a+b)*(a-b) == a*a - b*b; */ which is automatically discharged by alt-ergo. When I open the proof obligation in Coq, the lemma looks like follows: Goal forall (i_1 i : Z), (((i_1 * i_1) = ((i * i) + ((i + i_1) * (i_1 - i))))%Z)%Z. Under Neon the proof coq representation preserves the original names much better Goal forall (a_0 b_0 : Z), (((a_0 * a_0) = ((b_0 * b_0) + ((a_0 + b_0) * (a_0 - b_0))))%Z)%Z. The problem gets worse with more parameters.
Steps To Reproduceframa-c-gui -wp lemma.c
TagsNo tags attached.
Attached Filesc file icon lemma.c [^] (70 bytes) 2015-03-31 17:15 [Show Content]

- Relationships
related to 0002153acknowledgedcorrenson bound variable names in Coq file depend on unrelated function later in C source code 

-  Notes
(0005837)
jens (reporter)
2015-03-31 17:21

 I wonder whether this is related to my previous request for "better" coq names... https://bts.frama-c.com/view.php?id=1630
(0005877)
jens (reporter)
2015-04-10 10:39

 The "obfuscated" names generated by WP make it quite hard to work on coq proofs for functions with several arguments. Would it be possible to return to the naming scheme of Neon?
(0005879)
correnson (manager)
2015-04-10 11:16

 No it is not that easy. We need to find a solution to keep user names while still preserving our new very efficient locally-nameless implementation of binders in Qed...
(0005961)
correnson (manager)
2015-06-29 17:16

 We plan de completely rewrite the Coq output of goals to make them more readable.
(0006465)
Jochen (reporter)
2017-10-09 17:19

 I suspect that the (different) renaming (in lemmas and goals) even may lead to a worse verification rate, cf. issue #2329 for details.
(0006913)
correnson (manager)
2019-10-17 17:36

 Coq output is now deprecated and will be abandoned in future releases.

- Issue History
Date Modified Username Field Change
2015-03-31 17:15 jens New Issue
2015-03-31 17:15 jens Status new => assigned
2015-03-31 17:15 jens Assigned To => correnson
2015-03-31 17:15 jens File Added: lemma.c
2015-03-31 17:21 jens Note Added: 0005837
2015-04-10 10:39 jens Note Added: 0005877
2015-04-10 11:16 correnson Note Added: 0005879
2015-06-29 17:16 correnson Note Added: 0005961
2015-06-29 17:16 correnson Status assigned => acknowledged
2015-09-01 12:03 correnson Relationship added related to 0002153
2017-10-09 17:19 Jochen Note Added: 0006465
2019-10-17 17:36 correnson Note Added: 0006913
2019-10-17 17:36 correnson Status acknowledged => resolved
2019-10-17 17:36 correnson Resolution open => won't fix
2019-10-17 18:03 signoles Status resolved => closed

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker