0001328: Incorrect AST in presence of local ghost variables

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001328

Frama-C

Kernel > ACSL implementation

public

2012-12-13 09:51

2013-04-19 11:05

Reporter

signoles

Assigned To

virgile

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Target Version

Fixed in Version

Frama-C Fluorine-20130401

Summary

0001328: Incorrect AST in presence of local ghost variables

Description

$ less tests/syntax/ghost_lexing.i
int G = 0;

const char* foo = "foo";

void test(const char */*name*/);

void test2(int x) {
  /*@ ghost
    int y = 0;
    if (x>0) { y = x * x; };
  */
  G = x * x;
  test(foo);
}

$ frama-c -print tests/syntax/ghost_lexing.i
/* Generated by Frama-C */
int G = 0;
char const *foo = "foo";
extern void test(char const *);
void test2(int x)
{
  int y;
  y = 0;
  if (x > 0) { /*@ ghost y = x * x; */ }
  G = x * x;
  test(foo);
  return;
}

Tags

No tags attached.

Attached Files

Relationships

Notes
(0003630) signoles (manager) 2012-12-18 09:53	The issue occurs for any ghost declaration (even for global declarations).

Issue History
Date Modified	Username	Field	Change
2012-12-13 09:51	signoles	New Issue
2012-12-13 09:51	signoles	Status	new => assigned
2012-12-13 09:51	signoles	Assigned To	=> virgile
2012-12-18 09:53	signoles	Note Added: 0003630
2013-02-01 15:59	svn	Checkin
2013-02-01 15:59	svn	Status	assigned => resolved
2013-02-01 15:59	svn	Resolution	open => fixed
2013-04-19 11:05	signoles	Fixed in Version	=> Frama-C Fluorine
2013-04-19 11:05	signoles	Status	resolved => closed