--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on February 2010 ---
brackets<br> 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 ].<br> It is a debugging information.<br> <br> In fact, it is impossible to know if a mark computed by the slicer is imprecise or not. <br> Only the user or a second analysis of the slicing output can infer that! <br> <br> It is also the case for the spare statements even if they "<i>don't impact the slicing<br> criteria</i>". Of course, you can say: "<i>since these spare statements don't impact the <br> slicing criteria, I can remove it".</i> But if you want to perform a new analysis on<br> the resulting code, you <b>**must</b>** keep these statements otherwise, the<br> second analyser may reject that code. By second analyser, I include <br> compilers (otherwise, gcc may reject the sliced code), code executions<br> (otherwise, the binary got from the sliced code may crash). <br> I will try to give you an example soon.<br> <br> Patrick.<br> <pre class="moz-signature" cols="72">-- Patrick Baudin, CEA, LIST, SOL, F-91191 Gif-sur-Yvette cedex, France. tel: +33 (0)1 6908 2072 </pre> </body> </html> --------------050504030103050808070002--