Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 03:42 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000800Frama-CPlug-in > RTEpublic2011-10-10 14:14
Reporterpatrick 
Assigned Topherrmann 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
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

-Relationships
+Relationships

-Notes

~0001794

pherrmann (reporter)

Should be corrected as of svn 12931
+Notes

-Issue History
Date Modified Username Field Change
2011-04-18 14:14 patrick New Issue
2011-04-18 14:14 patrick Status new => assigned
2011-04-18 14:14 patrick Assigned To => pherrmann
2011-04-18 17:26 pherrmann Note Added: 0001794
2011-04-18 17:26 pherrmann Status assigned => resolved
2011-05-16 17:26 signoles Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
+Issue History