2020-12-05 00:19 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002297Frama-CKernelpublic2017-05-08 16:162017-12-06 09:10
ReporterJochen 
Assigned Tomaroneze 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon synt.c (125 bytes) 2017-05-08 16:16 - 
    int sum(void) {
	int s = 0
	/*@
		loop assigns i,s;
		loop variant 9-i;
	*/
	for (int i=0; i<9; ++i)
		s += 2;
	return s;
}
    c file icon synt.c (125 bytes) 2017-05-08 16:16 +

-Relationships
+Relationships

-Notes

~0006396

maroneze (administrator)

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;
+Notes

-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
2017-12-06 09:10 signoles Status resolved => closed
+Issue History