Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000588Frama-CKernelpublic2010-09-21 18:252014-02-12 16:55
Reporterdpariente 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000588: Error when function contract defined after function definition and with different parameter names
DescriptionAnalyzing this code:

void f(int a){ a=1;}
//@ ensures x>0;
void f(int x);

with:
frama-c foo.c

generates the following error message:
e1.c:4:[kernel] user error: unbound logic variable x in annotation.
[kernel] user error: skipping file "e1.c" that has errors.
[kernel] Frama-C aborted because of invalid user input.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-09-21 18:25 dpariente New Issue
2010-09-22 13:46 virgile Assigned To => virgile
2010-09-22 13:46 virgile Status new => confirmed
2010-10-06 15:16 svn Checkin
2010-10-06 15:16 svn Status confirmed => resolved
2010-10-06 15:16 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:35 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker