Frama-C Bug Tracking System - Frama-C
View Issue Details
0000620Frama-CKernelpublic2010-11-05 15:112010-12-17 19:35
patrick 
patrick 
normalminoralways
closedfixed 
Frama-C Boron-20100401 
Frama-C Carbon-20101201-beta1 
0000620: Default assigns generation
Today, 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.
With 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);
No tags attached.
Issue History
2010-11-05 15:11patrickNew Issue
2010-11-05 15:15patrickStatusnew => assigned
2010-11-05 15:15patrickAssigned To => patrick
2010-11-08 08:49patrickNote Added: 0001261
2010-11-08 08:49patrickStatusassigned => resolved
2010-11-08 08:49patrickResolutionopen => fixed
2010-12-10 15:45signolesFixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:35signolesStatusresolved => closed

Notes
(0001261)
patrick   
2010-11-08 08:49   
Revision 10452: trunk/src/logic/infer_annotations.ml