Frama-C Bug Tracking System - Frama-C
View Issue Details
0000800Frama-CPlug-in > RTEpublic2011-04-18 14:142011-10-10 14:14
patrick 
pherrmann 
normalminorhave not tried
closedfixed 
 
Frama-C Nitrogen-20111001 
0000800: wrong generation of assigns \nothing at function call
RTE should not generate assigns \nothing; at the statement calling function f
> 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; }
No tags attached.
Issue History
2011-04-18 14:14patrickNew Issue
2011-04-18 14:14patrickStatusnew => assigned
2011-04-18 14:14patrickAssigned To => pherrmann
2011-04-18 17:26pherrmannNote Added: 0001794
2011-04-18 17:26pherrmannStatusassigned => resolved
2011-05-16 17:26signolesResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed

Notes
(0001794)
pherrmann   
2011-04-18 17:26   
Should be corrected as of svn 12931