Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000620Frama-CKernelpublic2010-11-05 15:112010-12-17 19:35
Reporterpatrick 
Assigned Topatrick 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000620: Default assigns generation
DescriptionToday, Frama-C kernel generates assigns clauses from the prototype (for function without code).
To do nothing is equivalent to virtually generate "assigns everything".
That is not good for some static analysis (such as Value analysis).
When behaviors are completes and each of them has an assigns clause,
it is possible to generate a more restrictive clause (than "assigns everything"), but still correct:
"assigns locs;"
where "locs" is the union of the locations assigned by all behaviors of the complete clause.
Additional InformationWith this example, the clause "assigns *b" can be added to the default behavior.
requires \valid(b);
behavior positive:
assumes a > 0;
assigns *b;
ensures *b == 0;
behavior not_positive:
assumes a <= 0;
assigns \nothing;
complete behaviors;
disjoint behaviors;
*/ void foo(int a, int* b);
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001261)
patrick (developer)
2010-11-08 08:49

Revision 10452: trunk/src/logic/infer_annotations.ml

- Issue History
Date Modified Username Field Change
2010-11-05 15:11 patrick New Issue
2010-11-05 15:15 patrick Status new => assigned
2010-11-05 15:15 patrick Assigned To => patrick
2010-11-08 08:49 patrick Note Added: 0001261
2010-11-08 08:49 patrick Status assigned => resolved
2010-11-08 08:49 patrick Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:35 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker