Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000709Frama-CPlug-in > slicingpublic2011-02-08 05:442014-02-12 16:54
Reportertukarammuske 
Assigned ToAnne 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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 file icon testcase.c [^] (1,209 bytes) 2011-02-08 05:44 [Show Content]
? file icon Snapshot 2011-02-08 11-31-04.tiff [^] (65,324 bytes) 2011-02-08 11:33

- Relationships

-  Notes
(0001465)
pascal (reporter)
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 (reporter)
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 (reporter)
2011-02-08 08:52

Oh yes, sorry. I have reproduced the problem with Carbon-20110201.
(0001468)
pascal (reporter)
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 (reporter)
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 (reporter)
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
Date Modified Username Field Change
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-04-14 07:56 svn Checkin
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker