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 - 2019 MantisBT Team
Powered by Mantis Bugtracker