Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0001006Frama-CKernelpublic2011-11-02 13:082014-02-12 16:59
Reporteryakobowski 
Assigned Tovirgile 
PrioritylowSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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.
Relationships
related to 0000998closed yakobowski Invariant used only in absence of precondition 
Attached Files

Notes
(0002454)
virgile   
2011-11-07 18:16   
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)
   
2014-02-12 16:59   
Fix committed to stable/neon branch.

Issue History
Date ModifiedUsernameFieldChange
2011-11-02 13:08yakobowskiNew Issue
2011-11-02 13:09yakobowskiRelationship addedrelated to 0000998
2011-11-02 14:32yakobowskiStatusnew => assigned
2011-11-02 14:32yakobowskiAssigned To => virgile
2011-11-02 14:35yakobowskiDescription Updated
2011-11-07 18:16virgileNote Added: 0002454
2011-11-07 18:17svn
2011-11-07 18:17svnStatusassigned => resolved
2011-11-07 18:17svnResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2013-12-19 01:12Source_changeset_attached => framac master d07a7dbd
2014-02-12 16:54Source_changeset_attached => framac stable/neon d07a7dbd
2014-02-12 16:59Note Added: 0004716
2014-02-12 16:59Statusclosed => resolved