--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on February 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Frama-c-discus] on context sensitive points-to analysis



Myung-Jin wrote :
> I printed out slicing-marks by using -slicing-debug "-debug 2" option,
> and found that line 24's is [---][ S ]. Is this what you meant by
> "/imprecise/ ,but /correct?"
> Certainly all marks of relevant (to be more precise) statements
> contained at least one character inside the first brackets (one
> exception was that of slicing criterion line. It was [ S ][---]). This
> information might be used to filter out imprecise statements I think. If
> this understanding is not correct, please let me know.
>   
 From a user point of view, you should consider the union of the first 
brackets
and the second one. The distinction comes from the inter-procedural 
computation of slices. You can consider that there is no difference 
between marks [ S ][---] and [---][ S ].
It is a debugging information.

In fact, it is impossible to know if a mark computed by the slicer is 
imprecise or not.
Only the user or a second analysis of the slicing output can infer that!

It is also the case for the spare statements even if they "/don't impact 
the slicing
criteria/". Of course, you can say: "/since these spare statements don't 
impact the
slicing criteria, I can remove it"./ But if you want to perform a new 
analysis on
the resulting code, you ***must*** keep these statements otherwise, the
second analyser may reject that code. By second analyser, I include
compilers (otherwise, gcc may reject the sliced code), code executions
(otherwise, the binary got from the sliced code may crash).
I will try to give you an example soon.

Patrick.

-- 
Patrick Baudin,
CEA, LIST, SOL, F-91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100211/b9f5242b/attachment.htm