Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000482Frama-CKernel > ACSL implementationpublic2010-05-17 09:562010-12-17 19:38
Reporterpatrick 
Assigned Topatrick 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000482: for behav : invariant INV ;
DescriptionInvariant clauses can be associated to named behaviors like assert clauses.
Steps To Reproduce
Additional Information
TagsNo tags attached.
Relationships
Attached Files
Issue History
Date ModifiedUsernameFieldChange
2010-05-17 09:56patrickNew Issue
2010-05-17 09:56patrickStatusnew => assigned
2010-05-17 09:56patrickAssigned To => virgile
2010-05-17 09:57patrickAssigned Tovirgile => patrick
2010-05-17 09:59patrickNote Added: 0000852
2010-05-17 10:01patrickNote Added: 0000853
2010-05-17 10:01patrickStatusassigned => resolved
2010-05-17 10:01patrickFixed in Version => Frama-C svn, precise the release id
2010-05-17 10:01patrickResolutionopen => fixed
2010-12-10 15:40signolesFixed in VersionFrama-C GIT, precise the release id => Frama-C Carbon-20101201-beta1
2010-12-17 19:38signolesStatusresolved => closed

Notes
(0000852)
patrick   
2010-05-17 09:59   
svn commit -m "fixed #482" Sending cil/src/logic/logic_parser.mly Sending tests/spec/behavior_assert.c Sending tests/spec/oracle/behavior_assert.1.res.oracle Sending tests/spec/oracle/behavior_assert.res.oracle
(0000853)
patrick   
2010-05-17 10:01   
Committed revision 8724.