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]
- Subject: Sans objet
- From: email@example.com ()
- Date: Mon, 01 Feb 2010 09:28:40 -0000
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--