| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001630 | Frama-C | Plug-in > wp | public | 2014-01-23 19:27 | 2015-03-17 22:17 | ||||
| Reporter | jens | ||||||||
| Assigned To | correnson | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Fluorine-20130601 | ||||||||
| Target Version | Fixed in Version | Frama-C Sodium | |||||||
| Summary | 0001630: Make identifiers in Coq proofs more similar to those from C code | ||||||||
| Description | When 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.) | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
correnson (manager) 2014-02-05 13:13 |
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) 2014-02-05 13:15 |
Feature wish postponed to a future release. |
|
jens (reporter) 2014-03-16 18:32 |
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) 2014-06-02 17:05 Last edited: 2014-06-02 17:06 |
Fix committed to master branch. Only for short names (1 letter) with index 0. |
| Notes |
| 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 |