Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002297Frama-CKernelpublic2017-05-08 16:162017-05-31 19:19
ReporterJochen 
Assigned Tomaroneze 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformPhosphorus-20170501-beta1OSxubuntu 16.04.1OS Version
Product Version 
Target VersionFixed in VersionFrama-C 16 Sulfur 
Summary0002297: syntax error before loop contract reported after loop contract
DescriptionRunning "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.
TagsNo tags attached.
Attached Filesc file icon synt.c [^] (125 bytes) 2017-05-08 16:16 [Show Content]

- Relationships

-  Notes
(0006396)
maroneze (developer)
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;

- Issue History
Date Modified Username Field Change
2017-05-08 16:16 Jochen New Issue
2017-05-08 16:16 Jochen File Added: synt.c
2017-05-09 10:21 yakobowski Assigned To => maroneze
2017-05-09 10:21 yakobowski Status new => assigned
2017-05-23 13:34 maroneze Note Added: 0006396
2017-05-23 13:36 maroneze Status assigned => resolved
2017-05-23 13:36 maroneze Fixed in Version => Frama-C GIT, precise the release id
2017-05-23 13:36 maroneze Resolution open => fixed
2017-05-31 19:04 signoles Fixed in Version Frama-C GIT, precise the release id =>
2017-05-31 19:04 signoles Fixed in Version => Frama-C 15 Phosphorus
2017-05-31 19:05 signoles Status resolved => closed
2017-05-31 19:19 maroneze Status closed => resolved
2017-05-31 19:19 maroneze Fixed in Version Frama-C 15 Phosphorus => Frama-C 16 Sulfur


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker