0002297: syntax error before loop contract reported after loop contract

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002297

Frama-C

Kernel

public

2017-05-08 16:16

2017-05-31 19:19

Reporter

Jochen

Assigned To

maroneze

Priority

normal

Severity

minor

Reproducibility

always

Status

resolved

Resolution

fixed

Platform

Phosphorus-20170501-beta1

xubuntu 16.04.1

OS Version

Product Version

Target Version

Fixed in Version

Frama-C 16 Sulfur

Summary

0002297: syntax error before loop contract reported after loop contract

Description

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.

Tags

No tags attached.

Attached Files

synt.c [^] (125 bytes) 2017-05-08 16:16 [Show Content] [Hide Content]

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;
}

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