View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] |
ID | Project | Category | View Status | Date Submitted | Last Update |
0000568 | Frama-C | Kernel > ACSL implementation | public | 2010-08-23 14:53 | 2014-02-12 16:55 |
|
Reporter | derepas | |
Assigned To | virgile | |
Priority | normal | Severity | minor | Reproducibility | always |
Status | closed | Resolution | fixed | |
Platform | | OS | | OS Version | |
Product Version | Frama-C Boron-20100401 | |
Target Version | | Fixed in Version | Frama-C Carbon-20101201-beta1 | |
|
Summary | 0000568: cast to const type not handled in acsl annotations |
Description | Let 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).
|
Tags | No tags attached. |
|
Attached Files | |
|