Frama-C Bug Tracking System - Frama-C
View Issue Details
0000107Frama-CPlug-in > slicingpublic2009-05-27 16:382014-02-12 16:58
Frama-C GIT, precise the release id 
Frama-C Oxygen-20120901 
0000107: Slicer: slicing preserving some undesired function calls
(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);")!
No tags attached.
Issue History
2009-05-27 16:38dparienteNew Issue
2009-05-27 16:38dparienteStatusnew => assigned
2009-05-27 16:38dparienteAssigned To => Anne
2009-08-26 11:51AnneStatusassigned => confirmed
2011-12-22 12:01monateStatusconfirmed => assigned
2011-12-22 12:01monateAssigned ToAnne => yakobowski
2012-01-15 15:10yakobowskiNote Added: 0002578
2012-02-08 00:23svnCheckin
2012-02-08 00:23svnStatusassigned => resolved
2012-02-08 00:23svnResolutionopen => fixed
2012-02-08 00:31yakobowskiStatusresolved => feedback
2012-02-08 00:31yakobowskiResolutionfixed => reopened
2012-02-08 00:31yakobowskiStatusfeedback => resolved
2012-02-08 00:31yakobowskiResolutionreopened => fixed
2012-02-13 15:48yakobowskiRelationship addedrelated to 0001091
2012-02-23 18:11svnCheckin
2012-03-09 17:22svnCheckin
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2014-02-12 16:58yakobowskiNote Added: 0004677
2014-02-12 16:58yakobowskiStatusclosed => resolved

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?
2014-02-12 16:58   
Fix committed to stable/neon branch.