2021-02-24 18:59 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000620Frama-CKernelpublic2010-12-17 19:35
Assigned Topatrick 
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




patrick (developer)

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
+Issue History