Frama-C Bug Tracking System - Frama-C
View Issue Details
0000588Frama-CKernelpublic2010-09-21 18:252014-02-12 16:55
dpariente 
virgile 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Carbon-20101201-beta1 
0000588: Error when function contract defined after function definition and with different parameter names
Analyzing 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.
No tags attached.
Issue History
2010-09-21 18:25dparienteNew Issue
2010-09-22 13:46virgileAssigned To => virgile
2010-09-22 13:46virgileStatusnew => confirmed
2010-10-06 15:16svnCheckin
2010-10-06 15:16svnStatusconfirmed => resolved
2010-10-06 15:16svnResolutionopen => fixed
2010-12-10 15:45signolesFixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:35signolesStatusresolved => closed

There are no notes attached to this issue.