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.