Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002125Frama-CKernel > ACSL implementationpublic2015-06-01 21:232015-06-02 14:13
Reportergaggarwal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusconfirmedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0002125: Redefintion of variables in same scope is allowed in annotations
DescriptionConsider 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005928)
virgile (developer)
2015-06-02 14:13
edited on: 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.


- Issue History
Date Modified Username Field Change
2015-06-01 21:23 gaggarwal New Issue
2015-06-01 21:23 gaggarwal Status new => assigned
2015-06-01 21:23 gaggarwal Assigned To => virgile
2015-06-02 14:13 virgile Note Added: 0005928
2015-06-02 14:13 virgile Status assigned => confirmed
2015-06-02 14:13 virgile Note Edited: 0005928 View Revisions


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker