Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000505Frama-CKernel > ACSL implementationpublic2010-06-09 18:332014-02-12 16:55
Reportervirgile 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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? file icon constant_predicate.i [^] (148 bytes) 2010-06-09 18:33 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-06-09 18:33 virgile New Issue
2010-06-09 18:33 virgile Status new => assigned
2010-06-09 18:33 virgile Assigned To => virgile
2010-06-09 18:33 virgile File Added: constant_predicate.i
2010-06-09 18:35 virgile Status assigned => acknowledged
2010-06-09 18:38 svn Checkin
2010-06-10 19:18 svn Checkin
2010-06-10 19:18 svn Status acknowledged => resolved
2010-06-10 19:18 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker