|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0000709||Frama-C||Plug-in > slicing||public||2011-02-08 05:44||2014-02-12 16:54|
|Product Version||Frama-C Boron-20100401|
|Target Version||Fixed in Version||Frama-C Nitrogen-20111001|
|Summary||0000709: Bug in slicing -- required C-statements getting knocked off from sliced code|
|Description||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!!!)
|Additional Information||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.
|Tags||No tags attached.|
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.
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;.
|Oh yes, sorry. I have reproduced the problem with Carbon-20110201.|
|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).|
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
var1 FROM inp1 (and SELF)
var2 FROM inp1 (and SELF)
These seem normal (SELF is the new notation for var1, var2 depending on themselves).
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.
|2011-02-08 05:44||tukarammuske||New Issue|
|2011-02-08 05:44||tukarammuske||File Added: testcase.c|
|2011-02-08 07:39||pascal||Status||new => acknowledged|
|2011-02-08 07:49||pascal||Note Added: 0001465|
|2011-02-08 07:49||pascal||Status||acknowledged => feedback|
|2011-02-08 08:11||pascal||Note Edited: 0001465|
|2011-02-08 08:44||tukarammuske||Note Added: 0001466|
|2011-02-08 08:52||pascal||Note Added: 0001467|
|2011-02-08 08:52||pascal||Status||feedback => confirmed|
|2011-02-08 10:29||pascal||Status||confirmed => assigned|
|2011-02-08 10:29||pascal||Assigned To||=> Anne|
|2011-02-08 11:01||pascal||Assigned To||Anne => pascal|
|2011-02-08 11:11||pascal||Note Added: 0001468|
|2011-02-08 11:33||pascal||File Added: Snapshot 2011-02-08 11-31-04.tiff|
|2011-02-08 11:37||pascal||Note Added: 0001469|
|2011-02-08 11:37||pascal||Assigned To||pascal => Anne|
|2011-02-14 16:05||Anne||Note Added: 0001499|
|2011-02-14 16:05||Anne||Status||assigned => resolved|
|2011-02-14 16:05||Anne||Resolution||open => fixed|
|2011-02-16 11:50||signoles||Category||Kernel => Plug-in > slicing|
|2011-10-10 14:13||signoles||Fixed in Version||=> Frama-C Nitrogen-20111001|
|2011-10-10 14:14||signoles||Status||resolved => closed|
|2013-12-19 01:12||patrick||Source_changeset_attached||=> framac master ad280f53|
|2014-02-12 16:54||patrick||Source_changeset_attached||=> framac stable/neon ad280f53|