0001630: Make identifiers in Coq proofs more similar to those from C code - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ 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

Platform

OS

OS Version

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.

Relationships

Notes
(0004491) 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 "_" is reserved for local variables, whereas "" might clash with keywords, models and (unknown) user definitions.

(0004492) correnson (manager) 2014-02-05 13:15	Feature wish postponed to a future release.

(0004971) 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.

(0005189) correnson (manager) 2014-06-02 17:05 edited on: 2014-06-02 17:06	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	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

Copyright © 2000 - 2020 MantisBT Team