[Eva] User manual: completely removes the hidden section about -eva-no-results.

doc/value/examples/parametrizing/makefile

@@ -11,8 +11,6 @@ TARGETS = \
   widen-hints.log \
   slevel.1.log \
   slevel.2.log \
-  nor.1.log \
-  nor.2.log \
   ilevel.1.log \
   ilevel.2.log \
 	loop-unroll-const.log \
@@ -41,8 +39,3 @@ slevel.1.log: FCFLAGS += -slevel 55
 slevel.2.log: FCFLAGS += -slevel 28
 ilevel.2.log: FCFLAGS += -val-ilevel 16
 split-fabs.log: FCFLAGS += -eva-equality-domain
-
-nor.1.log nor.2.log: nor.c
-	time --format "\nuser time: %Us" $(FRAMAC) $(FCFLAGS) -val $< > $@ 2>&1
-nor.1.log: FCFLAGS += -slevel 2001
-nor.2.log: FCFLAGS += -slevel 2001 -no-results-function irrelevant_function

doc/value/examples/parametrizing/nor.c

-int t[2000], i;
-
-void irrelevant_function(void)
-{
-  for(i=0; i<2000; i++)
-    t[i]=i;
-}
-
-int main()
-{
-  irrelevant_function();
-
-  /* now the important stuff: */
-  return t[143];
-}

doc/value/main.tex

@@ -3621,97 +3621,6 @@ We have effectively replaced an alarm, the possible out-of-bounds access at
 line~7, by an invariant, that remains to be proven.
 
 
-%% \section{Treatment of functions}
-%% \label{trait_fonctions}
-
-%% Some \Eva{} options can be used to handle certain functions in a special
-%% way, to improve the efficiency of the analysis.
-
-
-%% \subsubsection{Skipping the recording of the results of a function}
-%% \label{noresults}
-
-%% When a function \lstinline|f|
-%% is called many times, or, in presence of semantic unrolling,
-%% if \lstinline|f| contains large/nested loops, significant 
-%% time may be spent recording the values taken by the program's variables
-%% at each of \lstinline|f|'s statements.
-%% If the user knows that these values will not be useful later,
-%% ey can instruct \Eva{} not to record these with the
-%% \lstinline|-eva-no-results-function f| option.
-%% The \lstinline|-eva-no-results-function| option
-%% can be used several times, to omit the results of several functions.
-%% The option \lstinline|-eva-no-results| can be used to omit all
-%% results.
-%% It can result in a significant saving of time, as in the following example.
-
-%% \lstinputlisting[numbers=left]
-%%   {examples/parametrizing/nor.c}
-
-%% \begin{shell}
-%% time frama-c -eva nor.c -eva-slevel 2001
-%% \end{shell}
-
-%% \lstinputlisting[linerange={30-33},numbers=left,firstnumber=36]
-%%   {examples/parametrizing/nor.1.log}
-%% \lstinputlisting[linerange={2032-2035},numbers=left,firstnumber=2036]
-%%   {examples/parametrizing/nor.1.log}
-%% \lstinputlisting[linerange={4032-4036},numbers=left,firstnumber=4038]
-%%   {examples/parametrizing/nor.1.log}
-
-%% Launched with option \lstinline|-eva-slevel 2001| so that the value returned
-%% by \lstinline|main| can be computed precisely, the analysis takes more than
-%% half a second.
-%%  Contrast with:
-
-%% \begin{shell}                                             
-%% time frama-c -eva nor.c -eva-slevel 2001 -eva-no-results-function irrelevant_function
-%% \end{shell}
-
-%% \lstinputlisting[linerange={30-34},numbers=left,firstnumber=36]
-%%   {examples/parametrizing/nor.2.log}
-%% \lstinputlisting[linerange={2031-2035},numbers=left,firstnumber=2037]
-%%   {examples/parametrizing/nor.2.log}
-
-%% When instructed, with 
-%% option \lstinline|-eva-no-results-function irrelevant_function|,
-%% that the values for the function
-%% \lstinline|irrelevant_function| do not need to be kept, \Eva{}
-%% takes less than half the time to produce its results. This shows
-%% that in the earlier analysis, most of the time was not spent in the
-%% analysis itself but in recording the values
-%% of \lstinline|irrelevant_function|.
-
-%% Note that the function \lstinline|irrelevant_function| was analyzed with
-%% as much precision as before, and that the result for \lstinline|main| is
-%% as precise as before. The recording of some results 
-%% is omitted, but this does not cause any loss of precision {\em during}
-%% the analysis\footnote{The emission of run-time error alarms and the evaluation
-%% of user-provided ACSL properties are done during the analysis and are 
-%% not influenced by the {\tt -eva-no-results*} options. If you make use
-%% of only these functionalities, then you can speed up the analysis 
-%% with option {\tt -eva-no-results} without detrimental effects.}.
-%% The results for \verb|irrelevant_function| are, as expected, unavailable.
-%% The ``outputs'' of \verb|main| (the ``outputs'' computation is
-%% described in chapter \ref{inoutdeps}) cannot be computed, because
-%% they depend on the outputs of \lstinline|irrelevant_function|, which
-%% require the values of that function to be computed.
-%% These outputs would automatically be used for
-%% displaying only the relevant variables if they were available.
-%% Instead, all the program's variables are displayed.
-
-%% The meaning of option \lstinline|-eva-no-results-function irrelevant_function|
-%% is different from that of option 
-%% \lstinline|-eva-slevel-function irrelevant_function:0|. In the case of the latter,
-%% values
-%% are computed with less precision for \verb|irrelevant_function|
-%% but the computed values are kept in memory as usual.
-%% All derived analyses (such as outputs)
-%% are available, but the values predicted by the analysis are
-%% less precise, because \verb|irrelevant_function| has been analyzed
-%% less precisely.
-
-
 \section{Improving precision with case-based reasoning}
 \label{trace-partitioning}