wrong generation of assigns \nothing at function call

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

---

Id	Project	Category	View	Due Date	Updated
ID0000800	Frama-C	Plug-in > RTE	public	2011-04-18	2011-10-10

Reporter	patrick	Assigned To	pherrmann	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	have not tried
Platform	-	OS	-	OS Version	-
Product Version	-	Target Version	-	Fixed in Version	Frama-C Nitrogen-20111001

Description :

RTE should not generate assigns \nothing; at the statement calling function f

Additional Information :

cat file.c: int X, Y ; //@ assigns \union(X, Y) ; void f () ; void g() { f () ; }

frama-c -print -rte file.c int X ; int Y ; /*@ assigns \union(X, Y); / extern void f() ; void g(void) { /@ behavior pre_f_0: assigns \nothing; */ f(); return; }