Frama-C Bug Tracking System - Frama-C
View Issue Details
0000505Frama-CKernel > ACSL implementationpublic2010-06-09 18:332014-02-12 16:55
Assigned Tovirgile 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000505: Predicate/Functions depending only on a state are not handled correctly
Descriptiona 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.
TagsNo tags attached.
Attached Files? constant_predicate.i (148) 2010-06-09 18:33

There are no notes attached to this issue.

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:38svn
2010-06-10 19:18svn
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
2013-12-19 01:13Source_changeset_attached => framac master bd8dc916
2013-12-19 01:13Source_changeset_attached => framac master 85452df2
2014-02-12 16:55Source_changeset_attached => framac stable/neon bd8dc916
2014-02-12 16:55Source_changeset_attached => framac stable/neon 85452df2