Frama-C Bug Tracking System - Frama-C
View Issue Details
0002125Frama-CKernel > ACSL implementationpublic2015-06-01 21:232015-06-02 14:13
gaggarwal 
virgile 
normalminoralways
confirmedopen 
Frama-C Neon-20140301 
 
0002125: Redefintion of variables in same scope is allowed in annotations
Consider an example: /*@ predicate is_valid(int* n, int n) = (0 <= n) ; */ Frama-C doesn't throw any exception for the above predicate, even though variable "n" is defined twice in the same scope and it uses n as of Type int and allows comparison 0 <= n. If I change the above predicate to following: /*@ predicate is_valid_int_range(int n, int* n) = (0 <= n) ; */ Frama-c complains "[kernel] user error: comparison of incompatible types: ℤ and int * in annotation" for comparison 0 <= n in above example, which means that it treats n of type int*. Similarly, redefinition of variable in same scope is allowed in quantifier expressions like: loop invariant \forall int k, char k; 0 <= k && k< i ==> a[k] == b[k]; In C language it is not allowed to redefine variable in same scope. Is this an intentional behavior? And if so that is the purpose behind it? I don't see this matter is discussed in ACSL document.
No tags attached.
Issue History
2015-06-01 21:23gaggarwalNew Issue
2015-06-01 21:23gaggarwalStatusnew => assigned
2015-06-01 21:23gaggarwalAssigned To => virgile
2015-06-02 14:13virgileNote Added: 0005928
2015-06-02 14:13virgileStatusassigned => confirmed
2015-06-02 14:13virgileNote Edited: 0005928View Revisions

Notes
(0005928)
virgile   
2015-06-02 14:13   
This is indeed a bug. Variables having the same scope should have distinct names in ACSL as well as in C. Thanks for the report.