2021-03-02 02:20 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000482Frama-CKernel > ACSL implementationpublic2010-12-17 19:38
Reporterpatrick 
Assigned Topatrick 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
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.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0000852

patrick (developer)

svn commit -m "fixed 0000482"
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 (developer)

Committed revision 8724.
+Notes

-Issue History
Date Modified Username Field Change
2010-05-17 09:56 patrick New Issue
2010-05-17 09:56 patrick Status new => assigned
2010-05-17 09:56 patrick Assigned To => virgile
2010-05-17 09:57 patrick Assigned To virgile => patrick
2010-05-17 09:59 patrick Note Added: 0000852
2010-05-17 10:01 patrick Note Added: 0000853
2010-05-17 10:01 patrick Status assigned => resolved
2010-05-17 10:01 patrick Fixed in Version => Frama-C svn, precise the release id
2010-05-17 10:01 patrick Resolution open => fixed
2010-12-10 15:40 signoles Fixed in Version Frama-C GIT, precise the release id => Frama-C Carbon-20101201-beta1
2010-12-17 19:38 signoles Status resolved => closed
+Issue History