2021-01-24 23:06 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001006Frama-CKernelpublic2014-02-12 16:59
Reporteryakobowski 
Assigned Tovirgile 
PrioritylowSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001006: Kernel should desugar "complete behaviors"
DescriptionCurrently, the kernel does not transform "complete behaviors;" clauses into "complete behaviors b1 ... bn;" when it sees one. However, this would be worthwhile:
- it makes life simpler for all the plugins, that have one less case to handle
- if someone adds some named behaviors programmatically, the "complete behaviors;" clause becomes less precise.
TagsNo tags attached.
Attached Files

-Relationships
related to 0000998closedyakobowski Invariant used only in absence of precondition 
+Relationships

-Notes

~0002454

virgile (developer)

Next commit will fix the bug, but at the same time slightly change the way such complete/disjoint clauses are handled when contract are split between various declarations: if we take the following file:

int x;

/*@ behavior a:
    assumes x >= 0;
*/
void f(void);

/*@ behavior b:
    assumes x < 0;
    complete behaviors;
*/
void f(void);

The old handling would treat the clause as complete behaviors a,b;, since it would operate on the merged contract resulting from both declarations. The new one considers that the only behavior involved in the implicit complete clause is b (the behavior that appears in the same contract as the clause). Naturally, it is always possible to explicitly state complete behaviors a,b;.

~0004716

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2011-11-02 13:08 yakobowski New Issue
2011-11-02 13:09 yakobowski Relationship added related to 0000998
2011-11-02 14:32 yakobowski Status new => assigned
2011-11-02 14:32 yakobowski Assigned To => virgile
2011-11-02 14:35 yakobowski Description Updated
2011-11-07 18:16 virgile Note Added: 0002454
2011-11-07 18:17 svn
2011-11-07 18:17 svn Status assigned => resolved
2011-11-07 18:17 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:12 Source_changeset_attached => framac master d07a7dbd
2014-02-12 16:54 Source_changeset_attached => framac stable/neon d07a7dbd
2014-02-12 16:59 Note Added: 0004716
2014-02-12 16:59 Status closed => resolved
+Issue History