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

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

Relationships

Notes

~0003630

signoles (manager)

2012-12-18 09:53

The issue occurs for any ghost declaration (even for global declarations).

Notes

Date Modified	Username	Field	Change
Issue History
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
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

Issue History