Frama-C Bug Tracking System - Frama-C
View Issue Details
0002297Frama-CKernelpublic2017-05-08 16:162017-12-06 09:10
Jochen 
maroneze 
normalminoralways
closedfixed 
Phosphorus-20170501-beta1xubuntu 16.04.1
 
Frama-C 16-Sulfur 
0002297: syntax error before loop contract reported after loop contract
Running "frama-c -wp synt.c" gives the output: [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing synt.c (with preprocessing) [kernel] syntax error at synt.c:7: 5 loop assigns i,s; 6 loop variant 9-i; 7 */ ^^^ 8 for (int i=0; i<9; ++i) 9 s += 2; [kernel] Frama-C aborted: invalid user input. This suggests that there is some syntax error within the loop contract (and it often takes a long time to check the contract byte by byte for correctness). However, the error is the missing semi-colon in line 3, immediately before the contract.
No tags attached.
c synt.c (125) 2017-05-08 16:16
https://bts.frama-c.com/file_download.php?file_id=1172&type=bug
Issue History
2017-05-08 16:16JochenNew Issue
2017-05-08 16:16JochenFile Added: synt.c
2017-05-09 10:21yakobowskiAssigned To => maroneze
2017-05-09 10:21yakobowskiStatusnew => assigned
2017-05-23 13:34maronezeNote Added: 0006396
2017-05-23 13:36maronezeStatusassigned => resolved
2017-05-23 13:36maronezeFixed in Version => Frama-C GIT, precise the release id
2017-05-23 13:36maronezeResolutionopen => fixed
2017-05-31 19:04signolesFixed in VersionFrama-C GIT, precise the release id =>
2017-05-31 19:04signolesFixed in Version => Frama-C 15-Phosphorus
2017-05-31 19:05signolesStatusresolved => closed
2017-05-31 19:19maronezeStatusclosed => resolved
2017-05-31 19:19maronezeFixed in VersionFrama-C 15-Phosphorus => Frama-C 16-Sulfur
2017-12-06 09:10signolesStatusresolved => closed

Notes
(0006396)
maroneze   
2017-05-23 13:34   
Thanks for the report. A patch has been devised that provides better error messages in this case, and in some other cases as well. However, this patch won't be available in Frama-C 15 (Phosphorus), only in Frama-C 16 (Sulfur). Here's what the new error message looks like: [kernel] syntax error at synt.c, between lines 3 and 7 1 2 int sum(void) { 3 int s = 0 4 /*@ 5 loop assigns i,s; 6 loop variant 9-i; 7 */ 8 for (int i=0; i<9; ++i) 9 s += 2;