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 context sensitive points-to analysis

  • Subject: [Frama-c-discuss] on context sensitive points-to analysis
  • From: myungjin at jung.tec.toyota.co.jp (jung, myung-jin)
  • Date: Thu, 11 Feb 2010 17:32:06 +0900
  • In-reply-to: <mailman.1364.1265815060.24779.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.1364.1265815060.24779.frama-c-discuss@lists.gforge.inria.fr>
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