cast to const type not handled in acsl annotations
ID0000568: This issue was created automatically from Mantis Issue 568. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000568 | Frama-C | Kernel > ACSL implementation | public | 2010-08-23 | 2014-02-12 |
| Reporter | derepas | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | Frama-C Carbon-20101201-beta1 |
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).