Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000107Frama-CPlug-in > slicingpublic2009-05-27 16:382014-02-12 16:58
Reporterdpariente 
Assigned Toyakobowski 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000107: 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);")!
TagsNo tags attached.
Attached Files

- 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 - 2019 MantisBT Team
Powered by Mantis Bugtracker