Frama-C Bug Tracking System - Frama-C
View Issue Details
0000800Frama-CPlug-in > RTEpublic2011-04-18 14:142011-10-10 14:14
Reporterpatrick 
Assigned Topherrmann 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000800: wrong generation of assigns \nothing at function call
DescriptionRTE 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;
}


TagsNo tags attached.
Attached Files

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

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