Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000605Frama-CKernel > ACSL implementationpublic2010-10-13 14:212010-12-16 10:05
Reporterboris 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000605: Empty specification causes syntax error
DescriptionFile [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.
TagsNo 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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker