0000800: wrong generation of assigns \nothing at function call

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000800

Frama-C

Plug-in > RTE

public

2011-04-18 14:14

2011-10-10 14:14

Reporter

patrick

Assigned To

pherrmann

Priority

normal

Severity

minor

Reproducibility

have not tried

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Target Version

Fixed in Version

Frama-C Nitrogen-20111001

Summary

0000800: wrong generation of assigns \nothing at function call

Description

RTE 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;
}

Tags

No 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