Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000568Frama-CKernel > ACSL implementationpublic2010-08-23 14:532014-02-12 16:55
Reporterderepas 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000568: cast to const type not handled in acsl annotations
DescriptionLet us consider the following file "ex.c" :
1 : int main() {
2 : const char * p1="foo1";
3 : //@ assert (\valid_index( (const char * ) p1,0));
4 : return 0;
5 : }
Then the command line "frama-c ex.c" yields the following error :
ex.c:3:[kernel] user error: syntax error while parsing annotation

This is the same for the following types : (char const *) or (char * const).


TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001101)
virgile (developer)
2010-08-25 14:39

const is now recognized in casts in ACSL. Since the logic do not contain mutable values, T and const T are considered equivalent though.

- Issue History
Date Modified Username Field Change
2010-08-23 14:53 derepas New Issue
2010-08-23 14:53 derepas Status new => assigned
2010-08-23 14:53 derepas Assigned To => virgile
2010-08-24 21:22 svn Checkin
2010-08-25 14:39 virgile Note Added: 0001101
2010-08-25 14:39 virgile Status assigned => resolved
2010-08-25 14:39 virgile Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:35 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker