Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
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

- Relationships

-  Notes
(0001794)
pherrmann (reporter)
2011-04-18 17:26

Should be corrected as of svn 12931

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker