0000107: Slicer: slicing preserving some undesired function calls - Frama-C Bug Tracking System

Frama-C Bug Tracking System

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

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0000107

Frama-C

Plug-in > slicing

public

2009-05-27 16:38

2014-02-12 16:58

Reporter

dpariente

Assigned To

yakobowski

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Oxygen-20120901

Summary

0000107: Slicer: slicing preserving some undesired function calls

Description

(This issue was previously discussed through private messages but not yet resolved. It was noticed that a solution would require some "work around"! It is now recorded into the BTS for traceability reasons.)

The following code is sliced w.r.t. its annotation.

typedef struct { int i; int j; } las;
las v1,v2,v3;

void g(las*p) { p->i = p->i * 2; }

void f()
{
  g( &v1 );
  g( &v2 );
  g( &v3 );
//@ assert v2.i>=10;
}

Command line:
frama-c -slice-assert f -slice-print -lib-entry -main f foo.c

The sliced code got rid of the statement g(&v3) (with calldeps), but kept g(&v1).
A slicer improvement would be, of course, to be able to get also rid of the 1st call to g (i.e., "g(&v1);")!

Tags

No tags attached.

Relationships

Notes
(0002578) yakobowski (manager) 2012-01-15 15:10	My diagnostic is that a "-call-pdg" option is needed to handle this properly. However, I would love to be proven wrong, as this would be an invasive and complicated change --- not to mention of amount of time and memory it might require at execution. Could someone point to me a document that explains how the slicing currently uses -calldeps to improve its results?

(0004677) yakobowski (manager) 2014-02-12 16:58	Fix committed to stable/neon branch.

Issue History
Date Modified	Username	Field	Change
2009-05-27 16:38	dpariente	New Issue
2009-05-27 16:38	dpariente	Status	new => assigned
2009-05-27 16:38	dpariente	Assigned To	=> Anne
2009-08-26 11:51	Anne	Status	assigned => confirmed
2011-12-22 12:01	monate	Status	confirmed => assigned
2011-12-22 12:01	monate	Assigned To	Anne => yakobowski
2012-01-15 15:10	yakobowski	Note Added: 0002578
2012-02-08 00:23	svn	Checkin
2012-02-08 00:23	svn	Status	assigned => resolved
2012-02-08 00:23	svn	Resolution	open => fixed
2012-02-08 00:31	yakobowski	Status	resolved => feedback
2012-02-08 00:31	yakobowski	Resolution	fixed => reopened
2012-02-08 00:31	yakobowski	Status	feedback => resolved
2012-02-08 00:31	yakobowski	Resolution	reopened => fixed
2012-02-13 15:48	yakobowski	Relationship added	related to 0001091
2012-02-23 18:11	svn	Checkin
2012-03-09 17:22	svn	Checkin
2012-09-19 17:15	signoles	Fixed in Version	=> Frama-C Oxygen-20120901
2012-09-19 17:16	signoles	Status	resolved => closed
2014-02-12 16:58	yakobowski	Note Added: 0004677
2014-02-12 16:58	yakobowski	Status	closed => resolved

Copyright © 2000 - 2018 MantisBT Team