2021-03-03 02:31 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001006Frama-CKernelpublic2014-02-12 16:59
Assigned Tovirgile 
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

related to 0000998closedyakobowski Invariant used only in absence of precondition 



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;.


Fix committed to stable/neon branch.

-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