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

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



Dear Patrick and Pascal,
Thank you for your comments. I confirmed what you have mentioned:
> Looking at the result given by the gui with the
> development version of Frama-C, line 24 isn't green,
> nor striked out. That means the semantics of the line 24
> doesn't impact the slicing criteria, but the line must be keept
> just for compilation reason (to be able to re-analyse code
> resulting from the slicing pulgin). These kinds of lines have
> a spare mark. Going back to your example, the spare
> mark of the line 24 is /imprecise/, but /correct.
>
> /Patrick.
>
>   
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.

> The only workaround that we can offer for the moment is to slice again
> on the same criterion a second time:
>
> frama-c -lib-entry -slice-pragma main -slice-print -quiet t.c
> -calldeps -ocode t2.c
> frama-c -lib-entry -slice-pragma main -slice-print -quiet t2.c -calldeps
>
> This removes anything related to s2t_1.
>
> We will look at the behavior you have reported.
>
> Pascal
>   

Thank you for your comments on PDGs, and a possible workaround. I tested
it and confirmed it worked. Slicing twice or referring the slicing-marks
might be two alternative solutions to the issue I think. Thank you.


Myung-Jin