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]

Sans objet

brackets<br>
and the second one.&nbsp; The distinction comes from the inter-procedural
computation of slices.&nbsp; 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>
&nbsp;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&nbsp; 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--