0000605: Empty specification causes syntax error

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000605

Frama-C

Kernel > ACSL implementation

public

2010-10-13 14:21

2010-12-16 10:05

Reporter

boris

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

always

Status

assigned

Resolution

open

Platform

OS Version

Product Version

Frama-C Boron-20100401

Target Version

Fixed in Version

Summary

0000605: Empty specification causes syntax error

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.

Tags

No tags attached.

Attached Files

Relationships

Notes
(0001188) pascal (reporter) 2010-10-13 14:33	The command-line frama-c t.c is enough to produce the problem. The value analysis does not have anything to do with it. Boris: the -jessie option causes a lot of things to happen. It is not surprising that it hides some bugs.

Issue History
Date Modified	Username	Field	Change
2010-10-13 14:21	boris	New Issue
2010-10-13 14:31	pascal	Status	new => assigned
2010-10-13 14:31	pascal	Assigned To	=> virgile
2010-10-13 14:33	pascal	Note Added: 0001188
2010-10-13 14:35	pascal	Summary	Empty specification causes syntax error in value analysis => Empty specification causes syntax error
2010-12-16 10:05	signoles	Category	Kernel => Kernel > ACSL implementation