2020-12-05 01:11 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000107Frama-CPlug-in > slicingpublic2014-02-12 16:58
Reporterdpariente 
Assigned Toyakobowski 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0002578

yakobowski (manager)

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)

Fix committed to stable/neon branch.
+Notes

-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
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-23 18:11 svn
2012-03-09 17:22 svn
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master 3074914f
2013-12-19 01:12 yakobowski Source_changeset_attached => framac master ff592c25
2014-02-12 16:54 yakobowski Source_changeset_attached => framac stable/neon 3074914f
2014-02-12 16:54 yakobowski Source_changeset_attached => framac stable/neon ff592c25
2014-02-12 16:58 yakobowski Note Added: 0004677
2014-02-12 16:58 yakobowski Status closed => resolved
+Issue History