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
Assigned Tovirgile 
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
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 - 2020 MantisBT Team
Powered by Mantis Bugtracker