GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0000731	Frama-C	Kernel	public	2011-02-18	2011-02-20

Reporter	Jonathan-Christofer Demay	Assigned To	virgile	Resolution	no change required
Priority	normal	Severity	minor	Reproducibility	have not tried
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Carbon-20110201	Target Version	-	Fixed in Version	-

Description :

I guess an example is enough to explain the problem:

/*@ behavior generated: assigns *b; assigns \at(\result,Post) \from *b, a; assigns *b \from *b, a;

*/ extern int func1(int a , int b ) ; /@ behavior generated: assigns \at(\result,Post) \from \nothing; */ extern int func2(int , int * ) ; void main(void) { func1(0,(int *)0); func2(0,(int *)0); return; }