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