--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on February 2010 ---
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