2021-03-02 02:26 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000568Frama-CKernel > ACSL implementationpublic2010-08-23 14:532014-02-12 16:55
Reporterderepas 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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
+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.
+Notes

-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
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
2013-12-19 01:12 Source_changeset_attached => framac master 9dc57d20
2014-02-12 16:55 Source_changeset_attached => framac stable/neon 9dc57d20
+Issue History