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] [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