Frama-C Bug Tracking System - Frama-C
View Issue Details
0000709Frama-CPlug-in > slicingpublic2011-02-08 05:442014-02-12 16:54
Assigned ToAnne 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000709: Bug in slicing -- required C-statements getting knocked off from sliced code
DescriptionThe frama-c is used for slicing of the attached testcase. The required C-statements, nondets of var1 and var2 (line 54 & 55, function inputsOf_testcase_func) are getting removed from sliced code. Actually they should not. Looks like theres bug in the frama-c slicing.

Also, it is observed that if any one of the block of code ( three blocks are mentioned in the testcase with comment Block-1,2 or 3) is deleted, the required nondets of var1 and var2 are seen in the sliced code (that is slicing is done correctly!!!)
Additional InformationThe command used to run frama-c is --

frama-c -slice-print -no-unicode -slice-pragma func testcase.c

The required details like problem, the blocks affecting the slicing, the knocked off c statements are described with comments in the attached test case.
TagsNo tags attached.
Attached Filesc testcase.c (1,209) 2011-02-08 05:44
? Snapshot 2011-02-08 11-31-04.tiff (65,324) 2011-02-08 11:33

2011-02-08 07:49   
(Last edited: 2011-02-08 08:11)
What makes you say that the statements var1 = nondet_int ( ); and var2 = nondet_int ( ); should be kept? They seem to me to be unnecessary for the provided slicing criterion, as var1, var2 are assigned in all branches of func before the /*@ slice pragma stmt; */ is reached.

A less efficient slicer would keep these assignments, but they do not seem necessary.

Please detail the problem you see.

2011-02-08 08:44   
We find the statements "var1 = nondet_int ( );" and "var2 = nondet_int ( );" are necessary as there exists a path where the variables var1 and var2 remain unassigned.

Considering inp1 taking value 10 ( any value other than 1,2,3), the path taken would include else branch of each if condition where no assignments are made to the var1 and var2. Thus the variables var1 and var2 will remain unassigned before the /*@ slice pragma stmt; */ is reached. We think that these nondet statements in turn will be required to preserve the effect of the next statement,
that is, 65 != var2 ? assert ( 5 != var1):1;.
2011-02-08 08:52   
Oh yes, sorry. I have reproduced the problem with Carbon-20110201.
2011-02-08 11:11   
Actually, a /*@ slice pragma stmt; */ is a slicing directive to preserve the *effects* of the following statement (which is an expression, so I am not sure what that means in that case). I tried using -slice-calls assert whose action is clearer to me on this program, and the result is the same (var1, var2 initializations are sliced when they clearly shouldn't be).
2011-02-08 11:37   
Anne: there seems to be something wrong with the PDG of func (see screenshot). var1 and var2 do not appear in input position, and I think they should.

I have checked the auxiliary analyses that the PDG depends on:

[inout] InOut (internal) for function func:
        Operational inputs: inp1; var1; var2
        Operational inputs on termination: inp1; var1; var2
      Function func:
         var1 FROM inp1 (and SELF)
         var2 FROM inp1 (and SELF)

These seem normal (SELF is the new notation for var1, var2 depending on themselves).
2011-02-14 16:05   
Thank you for your example : it has detected a very stupid bug (about state comparison during PDG computation).

Thanks also to Pascal to had a look at the problem.

Issue History
2011-02-08 05:44tukarammuskeNew Issue
2011-02-08 05:44tukarammuskeFile Added: testcase.c
2011-02-08 07:39pascalStatusnew => acknowledged
2011-02-08 07:49pascalNote Added: 0001465
2011-02-08 07:49pascalStatusacknowledged => feedback
2011-02-08 08:11pascalNote Edited: 0001465
2011-02-08 08:44tukarammuskeNote Added: 0001466
2011-02-08 08:52pascalNote Added: 0001467
2011-02-08 08:52pascalStatusfeedback => confirmed
2011-02-08 10:29pascalStatusconfirmed => assigned
2011-02-08 10:29pascalAssigned To => Anne
2011-02-08 11:01pascalAssigned ToAnne => pascal
2011-02-08 11:11pascalNote Added: 0001468
2011-02-08 11:33pascalFile Added: Snapshot 2011-02-08 11-31-04.tiff
2011-02-08 11:37pascalNote Added: 0001469
2011-02-08 11:37pascalAssigned Topascal => Anne
2011-02-14 16:05AnneNote Added: 0001499
2011-02-14 16:05AnneStatusassigned => resolved
2011-02-14 16:05AnneResolutionopen => fixed
2011-02-16 11:50signolesCategoryKernel => Plug-in > slicing
2011-04-14 07:56svn
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2013-12-19 01:12patrickSource_changeset_attached => framac master ad280f53
2014-02-12 16:54patrickSource_changeset_attached => framac stable/neon ad280f53