Frama-C Bug Tracking System - Frama-C
View Issue Details
0000505Frama-CKernel > ACSL implementationpublic2010-06-09 18:332014-02-12 16:55
virgile 
virgile 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Carbon-20101201-beta1 
0000505: Predicate/Functions depending only on a state are not handled correctly
a predicate with only a label (and no formals) can be applied as a variable (see attached file for examples). In this case, ACSL type-checker fails to attach to it the current default label.
No tags attached.
? constant_predicate.i (148) 2010-06-09 18:33
https://bts.frama-c.com/file_download.php?file_id=89&type=bug
Issue History
2010-06-09 18:33virgileNew Issue
2010-06-09 18:33virgileStatusnew => assigned
2010-06-09 18:33virgileAssigned To => virgile
2010-06-09 18:33virgileFile Added: constant_predicate.i
2010-06-09 18:35virgileStatusassigned => acknowledged
2010-06-09 18:38svnCheckin
2010-06-10 19:18svnCheckin
2010-06-10 19:18svnStatusacknowledged => resolved
2010-06-10 19:18svnResolutionopen => fixed
2010-12-10 15:45signolesFixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36signolesStatusresolved => closed

There are no notes attached to this issue.