Default assigns generation

ID0000620: This issue was created automatically from Mantis Issue 620. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000620	Frama-C	Kernel	public	2010-11-05	2010-12-17

Reporter	patrick	Assigned To	patrick	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Boron-20100401	Target Version	-	Fixed in Version	Frama-C Carbon-20101201-beta1

Description :

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);