Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
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.
Attached Files

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

-  Notes
(0002454)
virgile (developer)
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 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 Checkin
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
2014-02-12 16:59 Note Added: 0004716
2014-02-12 16:59 Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker