0000250: obfuscator loses link between logic and C variables

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000250

Frama-C

Plug-in > obfuscator

public

2009-09-18 15:59

2014-02-12 16:56

Reporter

virgile

Assigned To

monate

Priority

normal

Severity

major

Reproducibility

have not tried

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Beryllium-20090901

Target Version

Fixed in Version

Frama-C Beryllium-20090902

Summary

0000250: obfuscator loses link between logic and C variables

Description

on the code below,
//@ requires \valid(p);
void f(int * p);
int main(int * p)
{ f(p); }

executing frama-c -obfuscate t.c

returns
/*@ requires \valid(V1);
    */
extern void F1(int *G1 ) ;
int main(int *V3 )
{
  int V2 ;
  F1(V3);
  V2 = 0;
  return (V2);
}
i.e. the variable in the requires clause is not bound to the parameter of F1 anymore. It should be requires \valid(G1) instead.

Tags

No tags attached.

Attached Files

Relationships

Notes
(0000410) virgile (developer) 2009-09-21 11:46	This is only the case for specifications attached to prototypes.

Issue History
Date Modified	Username	Field	Change
2009-09-18 15:59	virgile	New Issue
2009-09-18 15:59	virgile	Status	new => assigned
2009-09-18 15:59	virgile	Assigned To	=> monate
2009-09-21 11:46	virgile	Note Added: 0000410
2009-09-21 15:05	svn	Checkin
2009-09-23 16:40	svn	Checkin
2009-09-23 16:40	svn	Status	assigned => resolved
2009-09-23 16:40	svn	Resolution	open => fixed
2009-09-23 16:41	signoles	Fixed in Version	=> Frama-C Beryllium 2
2009-09-23 20:22	signoles	Status	resolved => closed