View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
ID | Project | Category | View Status | Date Submitted | Last Update |
0000605 | Frama-C | Kernel > ACSL implementation | public | 2010-10-13 14:21 | 2010-12-16 10:05 |
|
Reporter | boris | |
Assigned To | virgile | |
Priority | normal | Severity | minor | Reproducibility | always |
Status | assigned | Resolution | open | |
Platform | | OS | | OS Version | |
Product Version | Frama-C Boron-20100401 | |
Target Version | | Fixed in Version | | |
|
Summary | 0000605: Empty specification causes syntax error |
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.
|
Tags | No tags attached. |
|
Attached Files | |
|