Default assigns generation
ID0000620: This issue was created automatically from Mantis Issue 620. Further discussion may take place here.
|Product Version||Frama-C Boron-20100401||Target Version||-||Fixed in Version||Frama-C Carbon-20101201-beta1|
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.
Additional Information :
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);