Frama-C Bug Tracking System - Frama-C
View Issue Details
0000709Frama-CPlug-in > slicingpublic2011-02-08 05:442014-02-12 16:54
tukarammuske 
Anne 
normalmajoralways
closedfixed 
Frama-C Boron-20100401 
Frama-C Nitrogen-20111001 
0000709: Bug in slicing -- required C-statements getting knocked off from sliced code
The 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!!!)
The 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.
No tags attached.
c testcase.c (1,209) 2011-02-08 05:44
https://bts.frama-c.com/file_download.php?file_id=163&type=bug
? Snapshot 2011-02-08 11-31-04.tiff (65,324) 2011-02-08 11:33
https://bts.frama-c.com/file_download.php?file_id=164&type=bug
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:56svnCheckin
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed

Notes
(0001465)
pascal   
2011-02-08 07:49   
(edited on: 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.
(0001466)
tukarammuske   
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;.
(0001467)
pascal   
2011-02-08 08:52   
Oh yes, sorry. I have reproduced the problem with Carbon-20110201.
(0001468)
pascal   
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).
(0001469)
pascal   
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 [from]... 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).
(0001499)
Anne   
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.