Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] on slicer outputs

jung, myung-jin wrote :
> Hello,

Hello,

> I am interested in obtaining PDG information of slicing results 
> to find out predecessor/successor relationships.

Well, I am not sure that my message was very clear yesterday...

You first have a PDG that gives predecessor/successor relationships.
This is independent from the slicing computation.
The slicing propagate kind of marks along the PDG edges,
and build a mapping between the PDG nodes and some marks.
 From these marks, we then know what statements have to be visible
in the slicing result.


> I have tried the following options so far:
> 1. "-pdg-debug -pdg" on original C code (before slicing)
> 2. "-slicing-debug "-debug 5"" in slicing the original C code.
> 
> The pdg information in 1. was fine, but I have no idea 
> how to link this pdg information to slicing debug info from 2. 

It is not very clear, I admit...

With the options : -slice-print -slicing-verbose 2
you get the slicing result annotated by the marks of the statements,
but it is not related to the PDG nodes:

For example, you get :
Print slice = f1_slice_1 : 
(InCtrl:<[-cd],[---]>)(In2:<[--d],[---]>)(OutRet:<[ S ],[---]>)
/**/int f1(/* <[---],[---]> */ int x , /* <[--d],[---]> */ int y )
           {
             /* <[---],[---]> */ int a ;
             /* <[--d],[---]> */ int b ;
             /* <[--d],[---]> */ int __retres ;
             /* <[---],[---]> */a = 1;
             /* <[--d],[---]> */b = 2;
             /* <[---],[---]> */G = x + a;
             /* <[--d],[---]> */__retres = y + b;
             /* <[ S ],[---]> */return (__retres);
           }

With the option : -slicing-debug 2
you get some more details about the computation step by step,
so you can find the final PDG marks of a slice by taking the last step.
For example :
[slicing] [Fct_Slice.after_marks_modifications] before:
Print slice = f2_slice_1
[slicing] 0 : <[-cd],[---]>
[slicing] 1 : <[---],[---]>
[slicing] 2 : <[---],[---]>
[slicing] 3 : <[--d],[---]>
[slicing] 4 : <[---],[---]>
[slicing] 5 : <[---],[---]>
[slicing] 6 : <[---],[---]>
[slicing] 7 : <[--d],[---]>
[slicing] 8 : <[-cd],[---]>
[slicing] 9 : <[---],[---]>
[slicing] 10 : <[--d],[---]>

The numbers 0-10 are the PDG nodes identifier,
and the <[...],[...]> is the slicing mark for this node
in the slice 1 of function f2.

> Or where to see in the source to find out related internal information.

The best place to look at in the source code is the PDG and Slicing API
defined in  src/kernel/db.mli (modules Pdg and Slicing of course...).

> Could you provide information on finding out immediate predecessor/successor 
 > relationships from slicing results?

If you are interested in the predecessor/successor relationships,
you only need the PDG results :
the slicing only uses these relationships, but doesn't change them.

Hope this help, but maybe it would be easier to help you
is you give an idea of what you want to do ?

Sincerely,
-- 
Anne.