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
Assigned Tovirgile 
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
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