Empty specification causes syntax error
ID0000605: This issue was created automatically from Mantis Issue 605. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000605 | Frama-C | Kernel > ACSL implementation | public | 2010-10-13 | 2010-12-16 |
| Reporter | boris | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | - |
Description :
File [1] causes error [2] when processed with frama-c -val. However, processing with frama-c -jessie causes no errors.
Additional Information :
[1]
int* p; int foo();
/*@
*/ int main() { int i, t[10];
for(i=0; i<=10; i++) t[i]=i;
if(foo()) p[2] = 1;
return 0; }
[2] [kernel] preprocessing with "gcc -C -E -I. val1.c" val1.c:6:[kernel] user error: syntax error while parsing annotation [kernel] user error: skipping file "val1.c" that has errors. [kernel] Frama-C aborted because of an invalid user input.