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
- Subject: [Frama-c-discuss] [Frama-c-discus] on context sensitive points-to analysis
- From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
- Date: Thu, 11 Feb 2010 10:47:24 +0100
- In-reply-to: <4B73C086.7010409@jung.tec.toyota.co.jp>
- References: <mailman.1364.1265815060.24779.frama-c-discuss@lists.gforge.inria.fr> <4B73C086.7010409@jung.tec.toyota.co.jp>
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
- References:
- [Frama-c-discuss] on context sensitive points-to analysis
- From: myungjin at jung.tec.toyota.co.jp (jung, myung-jin)
- [Frama-c-discuss] on context sensitive points-to analysis
- Prev by Date: [Frama-c-discuss] Frama-c-discuss Digest, Vol 21, Issue 6
- Next by Date: [Frama-c-discuss] on context sensitive points-to analysis
- Previous by thread: [Frama-c-discuss] on context sensitive points-to analysis
- Next by thread: [Frama-c-discuss] on context sensitive points-to analysis
- Index(es):