2021-01-27 11:46 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001630Frama-CPlug-in > wppublic2015-03-17 22:17
Assigned Tocorrenson 
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001630: Make identifiers in Coq proofs more similar to those from C code
DescriptionWhen I want to proof an obligation for function
  foo(int* a, int n)
then the Coq representation of the obligation uses the identifiers "a_0" and "n_0".
In my opinion, the proofs would be easier to read if WP would generate the names "a"
and "n".
(I often use "remember a_0 as a" to achieve this, but it would be nicer if I did not have to do it manually.)
TagsNo tags attached.
Attached Files




correnson (manager)

This is difficult to implement in a safe way. We need to avoid name clashes, and we rely on patterns to do this. Hence, pattern "<ident>_<number>" is reserved for local variables, whereas "<ident>" might clash with keywords, models and (unknown) user definitions.


correnson (manager)

Feature wish postponed to a future release.


jens (reporter)

Could this be done at least for the names in logic declarations in ACSL?
For example, the variable names of an axiom such as

    axiom CountUnion:
      \forall value_type *a, v, integer i, j, k;
        0 <= i <= j <= k ==> Count(a, v, i ,k) == Count(a, v, i, j) + Count(a, v, j, k);

looks like this on the Coq level

Q_CountUnion :
forall (i_0 j_0 k_0 v_0 : int) (Mint_0 : farray addr int) (a_0 : addr),
0 <= i_0 ->
i_0 <= j_0 ->
j_0 <= k_0 ->
is_sint32 v_0 ->
L_Count Mint_0 a_0 v_0 i_0 k_0 =
L_Count Mint_0 a_0 v_0 i_0 j_0 + L_Count Mint_0 a_0 v_0 j_0 k_0

It would be nice, if the arguments would read i, j, k, v, and a on the Coq-level.


correnson (manager)

Last edited: 2014-06-02 17:06

View 2 revisions

Fix committed to master branch.
Only for short names (1 letter) with index 0.


-Issue History
Date Modified Username Field Change
2014-01-23 19:27 jens New Issue
2014-01-23 19:27 jens Status new => assigned
2014-01-23 19:27 jens Assigned To => correnson
2014-02-05 13:13 correnson Note Added: 0004491
2014-02-05 13:15 correnson Note Added: 0004492
2014-02-05 13:15 correnson Status assigned => acknowledged
2014-03-16 18:32 jens Note Added: 0004971
2014-06-02 17:05 correnson Source_changeset_attached => framac master 4b98558c
2014-06-02 17:05 correnson Note Added: 0005189
2014-06-02 17:05 correnson Status acknowledged => resolved
2014-06-02 17:05 correnson Resolution open => fixed
2014-06-02 17:06 correnson Note Edited: 0005189 View Revisions
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:17 signoles Status resolved => closed
+Issue History