diff --git a/doc/value/div.c b/doc/value/examples/alarms/div.c
similarity index 100%
rename from doc/value/div.c
rename to doc/value/examples/alarms/div.c
diff --git a/doc/value/double_op_arg.c b/doc/value/examples/alarms/double_op_arg.c
similarity index 100%
rename from doc/value/double_op_arg.c
rename to doc/value/examples/alarms/double_op_arg.c
diff --git a/doc/value/double_op_res.c b/doc/value/examples/alarms/double_op_res.c
similarity index 100%
rename from doc/value/double_op_res.c
rename to doc/value/examples/alarms/double_op_res.c
diff --git a/doc/value/invalid.c b/doc/value/examples/alarms/invalid.c
similarity index 100%
rename from doc/value/invalid.c
rename to doc/value/examples/alarms/invalid.c
diff --git a/doc/value/invalid_bool.c b/doc/value/examples/alarms/invalid_bool.c
similarity index 100%
rename from doc/value/invalid_bool.c
rename to doc/value/examples/alarms/invalid_bool.c
diff --git a/doc/value/lshift.c b/doc/value/examples/alarms/lshift.c
similarity index 100%
rename from doc/value/lshift.c
rename to doc/value/examples/alarms/lshift.c
diff --git a/doc/value/ov_float_int.c b/doc/value/examples/alarms/ov_float_int.c
similarity index 100%
rename from doc/value/ov_float_int.c
rename to doc/value/examples/alarms/ov_float_int.c
diff --git a/doc/value/overlap.c b/doc/value/examples/alarms/overlap.c
similarity index 100%
rename from doc/value/overlap.c
rename to doc/value/examples/alarms/overlap.c
diff --git a/doc/value/pointer_comparison.c b/doc/value/examples/alarms/pointer_comparison.c
similarity index 100%
rename from doc/value/pointer_comparison.c
rename to doc/value/examples/alarms/pointer_comparison.c
diff --git a/doc/value/se.c b/doc/value/examples/alarms/se.c
similarity index 100%
rename from doc/value/se.c
rename to doc/value/examples/alarms/se.c
diff --git a/doc/value/shift.c b/doc/value/examples/alarms/shift.c
similarity index 100%
rename from doc/value/shift.c
rename to doc/value/examples/alarms/shift.c
diff --git a/doc/value/uninitialized.c b/doc/value/examples/alarms/uninitialized.c
similarity index 100%
rename from doc/value/uninitialized.c
rename to doc/value/examples/alarms/uninitialized.c
diff --git a/doc/value/valid_function.c b/doc/value/examples/alarms/valid_function.c
similarity index 100%
rename from doc/value/valid_function.c
rename to doc/value/examples/alarms/valid_function.c
diff --git a/doc/value/annotations_2.c b/doc/value/examples/annotations_2.c
similarity index 100%
rename from doc/value/annotations_2.c
rename to doc/value/examples/annotations_2.c
diff --git a/doc/value/ari.c b/doc/value/examples/ari.c
similarity index 100%
rename from doc/value/ari.c
rename to doc/value/examples/ari.c
diff --git a/doc/value/array.c b/doc/value/examples/array.c
similarity index 100%
rename from doc/value/array.c
rename to doc/value/examples/array.c
diff --git a/doc/value/array_array_2.c b/doc/value/examples/array_array_2.c
similarity index 100%
rename from doc/value/array_array_2.c
rename to doc/value/examples/array_array_2.c
diff --git a/doc/value/bases.c b/doc/value/examples/bases.c
similarity index 100%
rename from doc/value/bases.c
rename to doc/value/examples/bases.c
diff --git a/doc/value/boucles.c b/doc/value/examples/boucles.c
similarity index 100%
rename from doc/value/boucles.c
rename to doc/value/examples/boucles.c
diff --git a/doc/value/boucles1.c b/doc/value/examples/boucles1.c
similarity index 100%
rename from doc/value/boucles1.c
rename to doc/value/examples/boucles1.c
diff --git a/doc/value/boucles_run.c b/doc/value/examples/boucles_run.c
similarity index 100%
rename from doc/value/boucles_run.c
rename to doc/value/examples/boucles_run.c
diff --git a/doc/value/case.c b/doc/value/examples/case.c
similarity index 100%
rename from doc/value/case.c
rename to doc/value/examples/case.c
diff --git a/doc/value/default.c b/doc/value/examples/default.c
similarity index 100%
rename from doc/value/default.c
rename to doc/value/examples/default.c
diff --git a/doc/value/deps.c b/doc/value/examples/deps.c
similarity index 100%
rename from doc/value/deps.c
rename to doc/value/examples/deps.c
diff --git a/doc/value/depth.c b/doc/value/examples/depth.c
similarity index 100%
rename from doc/value/depth.c
rename to doc/value/examples/depth.c
diff --git a/doc/value/double_assign.c b/doc/value/examples/double_assign.c
similarity index 100%
rename from doc/value/double_assign.c
rename to doc/value/examples/double_assign.c
diff --git a/doc/value/exemple_origin_arithmetic.c b/doc/value/examples/exemple_origin_arithmetic.c
similarity index 100%
rename from doc/value/exemple_origin_arithmetic.c
rename to doc/value/examples/exemple_origin_arithmetic.c
diff --git a/doc/value/false_al.c b/doc/value/examples/false_al.c
similarity index 100%
rename from doc/value/false_al.c
rename to doc/value/examples/false_al.c
diff --git a/doc/value/fonctions.c b/doc/value/examples/fonctions.c
similarity index 100%
rename from doc/value/fonctions.c
rename to doc/value/examples/fonctions.c
diff --git a/doc/value/introduction.c b/doc/value/examples/introduction.c
similarity index 100%
rename from doc/value/introduction.c
rename to doc/value/examples/introduction.c
diff --git a/doc/value/leaf.c b/doc/value/examples/leaf.c
similarity index 100%
rename from doc/value/leaf.c
rename to doc/value/examples/leaf.c
diff --git a/doc/value/main.c b/doc/value/examples/main.c
similarity index 100%
rename from doc/value/main.c
rename to doc/value/examples/main.c
diff --git a/doc/value/merge.c b/doc/value/examples/merge.c
similarity index 100%
rename from doc/value/merge.c
rename to doc/value/examples/merge.c
diff --git a/doc/value/misa.c b/doc/value/examples/misa.c
similarity index 100%
rename from doc/value/misa.c
rename to doc/value/examples/misa.c
diff --git a/doc/value/no_propagation.c b/doc/value/examples/no_propagation.c
similarity index 100%
rename from doc/value/no_propagation.c
rename to doc/value/examples/no_propagation.c
diff --git a/doc/value/nondet.c b/doc/value/examples/nondet.c
similarity index 100%
rename from doc/value/nondet.c
rename to doc/value/examples/nondet.c
diff --git a/doc/value/op_inputs.c b/doc/value/examples/op_inputs.c
similarity index 100%
rename from doc/value/op_inputs.c
rename to doc/value/examples/op_inputs.c
diff --git a/doc/value/pad.c b/doc/value/examples/pad.c
similarity index 100%
rename from doc/value/pad.c
rename to doc/value/examples/pad.c
diff --git a/doc/value/perf.c b/doc/value/examples/perf.c
similarity index 100%
rename from doc/value/perf.c
rename to doc/value/examples/perf.c
diff --git a/doc/value/posix.c b/doc/value/examples/posix.c
similarity index 100%
rename from doc/value/posix.c
rename to doc/value/examples/posix.c
diff --git a/doc/value/reduction.c b/doc/value/examples/reduction.c
similarity index 100%
rename from doc/value/reduction.c
rename to doc/value/examples/reduction.c
diff --git a/doc/value/rte.c b/doc/value/examples/rte.c
similarity index 100%
rename from doc/value/rte.c
rename to doc/value/examples/rte.c
diff --git a/doc/value/s_t.c b/doc/value/examples/s_t.c
similarity index 100%
rename from doc/value/s_t.c
rename to doc/value/examples/s_t.c
diff --git a/doc/value/sq.c b/doc/value/examples/sq.c
similarity index 100%
rename from doc/value/sq.c
rename to doc/value/examples/sq.c
diff --git a/doc/value/termination.c b/doc/value/examples/termination.c
similarity index 100%
rename from doc/value/termination.c
rename to doc/value/examples/termination.c
diff --git a/doc/value/vraie_al.c b/doc/value/examples/vraie_al.c
similarity index 100%
rename from doc/value/vraie_al.c
rename to doc/value/examples/vraie_al.c
diff --git a/doc/value/gui-images-raw/RMB_click.svg b/doc/value/gui-images/RMB_click.svg
similarity index 100%
rename from doc/value/gui-images-raw/RMB_click.svg
rename to doc/value/gui-images/RMB_click.svg
diff --git a/doc/value/eval-acsl.png b/doc/value/gui-images/eval-acsl.png
similarity index 100%
rename from doc/value/eval-acsl.png
rename to doc/value/gui-images/eval-acsl.png
diff --git a/doc/value/gui-callstacks-annotated.png b/doc/value/gui-images/gui-callstacks-annotated.png
similarity index 100%
rename from doc/value/gui-callstacks-annotated.png
rename to doc/value/gui-images/gui-callstacks-annotated.png
diff --git a/doc/value/gui-images-raw/gui-callstacks.png b/doc/value/gui-images/gui-callstacks.png
similarity index 100%
rename from doc/value/gui-images-raw/gui-callstacks.png
rename to doc/value/gui-images/gui-callstacks.png
diff --git a/doc/value/gui-images-raw/gui-callstacks.svg b/doc/value/gui-images/gui-callstacks.svg
similarity index 100%
rename from doc/value/gui-images-raw/gui-callstacks.svg
rename to doc/value/gui-images/gui-callstacks.svg
diff --git a/doc/value/gui-loop-to-unroll.png b/doc/value/gui-images/gui-loop-to-unroll.png
similarity index 100%
rename from doc/value/gui-loop-to-unroll.png
rename to doc/value/gui-images/gui-loop-to-unroll.png
diff --git a/doc/value/gui-red-alarms-panel.png b/doc/value/gui-images/gui-red-alarms-panel.png
similarity index 100%
rename from doc/value/gui-red-alarms-panel.png
rename to doc/value/gui-images/gui-red-alarms-panel.png
diff --git a/doc/value/gui-red-values.png b/doc/value/gui-images/gui-red-values.png
similarity index 100%
rename from doc/value/gui-red-values.png
rename to doc/value/gui-images/gui-red-values.png
diff --git a/doc/value/gui-side-panel.png b/doc/value/gui-images/gui-side-panel.png
similarity index 100%
rename from doc/value/gui-side-panel.png
rename to doc/value/gui-images/gui-side-panel.png
diff --git a/doc/value/gui-values-annotated.png b/doc/value/gui-images/gui-values-annotated.png
similarity index 100%
rename from doc/value/gui-values-annotated.png
rename to doc/value/gui-images/gui-values-annotated.png
diff --git a/doc/value/gui-images-raw/gui-values.png b/doc/value/gui-images/gui-values.png
similarity index 100%
rename from doc/value/gui-images-raw/gui-values.png
rename to doc/value/gui-images/gui-values.png
diff --git a/doc/value/gui-images-raw/gui-values.svg b/doc/value/gui-images/gui-values.svg
similarity index 100%
rename from doc/value/gui-images-raw/gui-values.svg
rename to doc/value/gui-images/gui-values.svg
diff --git a/doc/value/gui1-annotated.pdf b/doc/value/gui-images/gui1-annotated.pdf
similarity index 100%
rename from doc/value/gui1-annotated.pdf
rename to doc/value/gui-images/gui1-annotated.pdf
diff --git a/doc/value/gui-images-raw/gui1-annotated.svg b/doc/value/gui-images/gui1-annotated.svg
similarity index 100%
rename from doc/value/gui-images-raw/gui1-annotated.svg
rename to doc/value/gui-images/gui1-annotated.svg
diff --git a/doc/value/gui-images-raw/gui1.png b/doc/value/gui-images/gui1.png
similarity index 100%
rename from doc/value/gui-images-raw/gui1.png
rename to doc/value/gui-images/gui1.png
diff --git a/doc/value/gui2.png b/doc/value/gui-images/gui2.png
similarity index 100%
rename from doc/value/gui2.png
rename to doc/value/gui-images/gui2.png
diff --git a/doc/value/gui3.png b/doc/value/gui-images/gui3.png
similarity index 100%
rename from doc/value/gui3.png
rename to doc/value/gui-images/gui3.png
diff --git a/doc/value/gui4.png b/doc/value/gui-images/gui4.png
similarity index 100%
rename from doc/value/gui4.png
rename to doc/value/gui-images/gui4.png
diff --git a/doc/value/gui5.png b/doc/value/gui-images/gui5.png
similarity index 100%
rename from doc/value/gui5.png
rename to doc/value/gui-images/gui5.png
diff --git a/doc/value/studia.png b/doc/value/gui-images/studia.png
similarity index 100%
rename from doc/value/studia.png
rename to doc/value/gui-images/studia.png
diff --git a/doc/value/gui.tex b/doc/value/gui.tex
index 62e1b8e87129388ad83eb8baecb4e56d81355141..4a767a5126cf2aa4a28b7c02dec4c8388bd982d7 100644
--- a/doc/value/gui.tex
+++ b/doc/value/gui.tex
@@ -39,7 +39,7 @@ indicate some parts that are never (or rarely) used with \Eva{}.
\begin{figure}[hbt]
\centering
-\includegraphics[width=\textwidth]{gui1-annotated.pdf}
+\includegraphics[width=\textwidth]{gui-images/gui1-annotated.pdf}
\caption{Frama-C GUI for \Eva{}}
\label{fig:gui-eva}
\end{figure}
@@ -64,7 +64,7 @@ The checkbox {\em Show list of red alarms} shows or hides the
\begin{figure}
\centering
-\includegraphics[scale=0.7]{gui-side-panel.png}
+\includegraphics[scale=0.7]{gui-images/gui-side-panel.png}
\caption{GUI side panel for \Eva{}}
\label{fig:gui-side-panel}
\end{figure}
@@ -85,7 +85,7 @@ non-terminating statement, which in our example is a call to
\begin{figure}[hbt]
\centering
-\includegraphics[width=\textwidth]{gui2.png}
+\includegraphics[width=\textwidth]{gui-images/gui2.png}
\caption{Unreachable code in the Frama-C GUI}
\label{fig:gui-unreachable}
\end{figure}
@@ -120,7 +120,7 @@ the most powerful inspection tool for the \Eva{} plug-in in the Frama-C GUI.
\begin{figure}[hbtp]
\centering
-\includegraphics[width=\textwidth]{gui-values-annotated.png}
+\includegraphics[width=\textwidth]{gui-images/gui-values-annotated.png}
\caption{Values panel}
\label{fig:values-panel}
\end{figure}
@@ -141,7 +141,7 @@ displayed in the \emph{Values} panel.
\begin{figure}[!hbtp]
\centering
-\includegraphics[scale=0.7]{eval-acsl.png}
+\includegraphics[scale=0.7]{gui-images/eval-acsl.png}
\caption{Evaluate ACSL term dialog, accessible via a context menu or
by pressing Ctrl+E.}
\label{fig:eval-acsl}
@@ -168,7 +168,7 @@ via right-clicks (Figure~\ref{fig:callstacks}).
\begin{figure}[hbtp]
\centering
-\includegraphics[width=\textwidth]{gui-callstacks-annotated.png}
+\includegraphics[width=\textwidth]{gui-images/gui-callstacks-annotated.png}
\caption{Callstacks display}
\label{fig:callstacks}
\end{figure}
@@ -202,7 +202,7 @@ the result displayed in Figure~\ref{fig:non-term-callstack}.
\begin{figure}[hbt]
\centering
-\includegraphics[width=\textwidth]{gui5.png}
+\includegraphics[width=\textwidth]{gui-images/gui5.png}
\caption{Focused on a non-terminating callstack}
\label{fig:non-term-callstack}
\end{figure}
@@ -245,7 +245,7 @@ indirect accesses.
\begin{figure}[h!]
\caption{\label{fig:studia}Studia elements in the GUI}
\centering
- \includegraphics[width=\textwidth]{studia}
+ \includegraphics[width=\textwidth]{gui-images/studia}
\end{figure}
Typical usage of Studia consists in: starting the GUI, selecting an alarm
@@ -321,7 +321,7 @@ status was emitted during the analysis.
\begin{figure}[htbp]
\centering
-\includegraphics[width=\textwidth]{gui-red-alarms-panel.png}
+\includegraphics[width=\textwidth]{gui-images/gui-red-alarms-panel.png}
\caption{Red alarms panel}
\label{fig:red-alarms-panel}
\end{figure}
@@ -335,7 +335,7 @@ the property evaluated to false at least once''.
\begin{figure}[htbp]
\centering
-\includegraphics[width=\textwidth]{gui-red-values.png}
+\includegraphics[width=\textwidth]{gui-images/gui-red-values.png}
\caption{Indicators of red alarms in the Values panel}
\label{fig:red-values}
\end{figure}
diff --git a/doc/value/main.idx b/doc/value/main.idx
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/doc/value/main.tex b/doc/value/main.tex
index 2cc8c362d514faeb329df932c57bb06fac788a5a..1ce3608b29a8fe3724a3ed8f62e4e49185fb76ae 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -119,7 +119,7 @@ code and observe an over-approximation of the set of
values this expression can take at run-time.
Here is a simple C example:
-\listinginputcaption{1}{\texttt{introduction.c}}{introduction.c}
+\listinginputcaption{1}{\texttt{introduction.c}}{examples/introduction.c}
If either interface of Frama-C is launched with options
\lstinline|-eva introduction.c|,
@@ -151,7 +151,7 @@ during the last forty years.
An analyzed application may contain run-time errors: divisions by zero,
invalid pointer accesses,\ldots
-\listinginputcaption{1}{\texttt{rte.c}}{rte.c}
+\listinginputcaption{1}{\texttt{rte.c}}{examples/rte.c}
When launched with \lstinline|frama-c -eva rte.c|,
\Eva{} emits a warning about an out-of-bound access at line 5:
@@ -658,7 +658,7 @@ as in the example below:
\begin{figure}[hbt]
\centering
-\includegraphics[width=0.75\textwidth]{gui-loop-to-unroll.png}
+\includegraphics[width=0.75\textwidth]{gui-images/gui-loop-to-unroll.png}
\caption{Estimating loop unroll bounds in the GUI}
\label{fig:gui-loop-to-unroll}
\end{figure}
@@ -1346,7 +1346,7 @@ previously written as a single write that modified the whole set of
bits exactly.
An example of a program leading to a misaligned read is the following:
-\listinginput{1}{misa.c}
+\listinginput{1}{examples/misa.c}
The value returned by the function \lstinline|main| is\\
\lstinline|{{ garbled mix of &{ x; y } (origin: Misaligned { misa.c:6 }) }}|.\\
The analyzer is by default configured for a 32-bit architecture,
@@ -1371,7 +1371,7 @@ alignments are fused together. In the example below,
the memory states from
the then branch and from the else branch contain in the array
\lstinline|t| some 32-bit addresses with incompatible alignments.
-\listinginput{1}{merge.c}
+\listinginput{1}{examples/merge.c}
The value returned by function \lstinline|main| is\\
\lstinline|{{ garbled mix of &{ x; y } (origin: Merge { merge.c:10 }) }}|.
@@ -1393,7 +1393,7 @@ The origin \lstinline$Arithmetic L$
indicates that arithmetic operations
take place without the analyzer being able to represent the result
precisely.
-\listinginput{1}{ari.c}
+\listinginput{1}{examples/ari.c}
In this example, the return value for \lstinline|f| is\\
\lstinline|{{ garbled mix of &{ x; y } (origin: Arithmetic { ari.c:4 }) }}|.
@@ -1425,7 +1425,7 @@ a dereferenced pointer is valid, it emits an alarm that expresses
that the pointer needs to be valid at that point. Likewise, direct
array accesses that may be invalid are flagged.
-\listinginput{1}{invalid.c}
+\listinginput{1}{examples/alarms/invalid.c}
In the above example, the analysis is not able to guarantee that
the memory accesses \lstinline|t[i]| and \lstinline|*p| are valid,
so it emits a proof obligation for each:
@@ -1465,7 +1465,7 @@ property that the divisor is different from zero when it continues
the analysis after this point.
The property expressed by an alarm may also not be taken into account
when it is not easy to do so.
-\listinginput{1}{div.c}
+\listinginput{1}{examples/alarms/div.c}
\begin{logs}
div.c:4: ... division by zero. assert (int)(x*y) != 0;
div.c:5: ... division by zero. assert x != 0;
@@ -1487,7 +1487,7 @@ indeed, processors are often built in a way that such an
operation does not produce the \lstinline|0| or \lstinline|-1|
result that could have been expected. Here is an example
of program with such an issue, and the resulting alarm:
-\listinginput{1}{shift.c}
+\listinginput{1}{examples/alarms/shift.c}
\begin{logs}
shift.c:4: ... invalid RHS operand for shift. assert 0 <= c < 32;
\end{logs}
@@ -1502,7 +1502,7 @@ and does not lead to an alarm by default.
However, the option \lstinline|-warn-right-shift-negative| can be used to
enable such alarms.
-\listinginput{1}{lshift.c}
+\listinginput{1}{examples/alarms/lshift.c}
\begin{logs}
[eva:alarm] lshift.c:4: Warning: invalid LHS operand for left shift. assert 0 <= x;
\end{logs}
@@ -1541,7 +1541,7 @@ or unsigned downcasts that may exceed the destination range.
An alarm is emitted when a floating-point value appears to exceed the
range of the integer type it is converted to.
-\listinginput{1}{ov_float_int.c}
+\listinginput{1}{examples/alarms/ov_float_int.c}
\begin{logs}
...
[eva:alarm] ov_float_int.c:6: Warning: overflow in conversion from floating-point
@@ -1560,7 +1560,7 @@ with a finite interval representing the result obtained
if excluding these possibilities. This interval, like
any other result, may be over-approximated. An example of this
first kind of alarm can be seen in the following example.
-\listinginput{1}{double_op_res.c}
+\listinginput{1}{examples/alarms/double_op_res.c}
\begin{shell}
frama-c -eva -main sum double_op_res.c
\end{shell}
@@ -1578,7 +1578,7 @@ from \lstinline|int*| to \lstinline|float*|. The emitted alarm
excludes the possibility of the bit sequence used as a the
argument representing \lstinline|NaN|, an infinite, or an address.
See the example below.
-\listinginput{1}{double_op_arg.c}
+\listinginput{1}{examples/alarms/double_op_arg.c}
\begin{shell}
frama-c -eva double_op_arg.c
\end{shell}
@@ -1606,7 +1606,7 @@ value of a local variable that has not been initialized, or
if it appears to manipulate the address of a local variable outside
of the scope of said variable. Both issues occur in the following
example:
-\listinginput{1}{uninitialized.c}
+\listinginput{1}{examples/alarms/uninitialized.c}
\Eva{} emits alarms for lines 5
(variable \lstinline|r| may be uninitialized)
and 13 (a dangling pointer to local variable \lstinline|t| is used).
@@ -1650,7 +1650,7 @@ the values 0 and 1, but any other value might be a trap representation, that is,
an object representation that does not represent a valid value of the type.
Trap representations can be created through unions or pointer casts.
-\listinginput{1}{invalid_bool.c}
+\listinginput{1}{examples/alarms/invalid_bool.c}
\begin{shell}
frama-c -eva invalid_bool.c
\end{shell}
@@ -1680,7 +1680,7 @@ accordingly to the emitted alarm. For instance, for the
quantity \lstinline|&x+2| must be reliably comparable to 0, the
analysis assumes that the result of the comparison is 1. The
consequences are visible when analyzing the following example:
-\listinginput{1}{pointer_comparison.c}
+\listinginput{1}{examples/alarms/pointer_comparison.c}
\Eva{} finds that this program does not terminate.
This seems incorrect because an actual execution will terminate
on most architectures.
@@ -1727,7 +1727,7 @@ the example \lstinline|y = *p + x++;|, the post-increment is defined
as long as \lstinline|*p| does not have any bits in common with
\lstinline|x|.
-\listinginput{1}{se.c}
+\listinginput{1}{examples/alarms/se.c}
\begin{shell}
frama-c -eva se.c -unspecified-access
\end{shell}
@@ -1781,7 +1781,7 @@ These limitations will be addressed in a future version.
Vaguely related to, but different from, undefined side-effects in expressions,
\Eva{} warns about the following program:
-\listinginput{1}{overlap.c}
+\listinginput{1}{examples/alarms/overlap.c}
The programmer thought implementation-defined behavior was invoked
in the above program, using an union to type-pun between structs S and T.
@@ -1829,7 +1829,7 @@ if it can give some meaning to the call. This is meant to account
for frequent misconceptions on type compatibility (e.g. \lstinline|void *|
and \lstinline|int *| are \emph{not} compatible).
-\listinginput{1}{valid_function.c}
+\listinginput{1}{examples/alarms/valid_function.c}
\begin{logs}
[eva:alarm] valid_function.c:9: Warning:
@@ -2165,7 +2165,7 @@ introduce approximations when analyzing a loop.
Let us assume, in the following lines, that the function \lstinline|c|
is unknown:
-\listinginput{1}{boucles.c}
+\listinginput{1}{examples/boucles.c}
The \Eva{} plug-in could provide the best possible sets of values
if the user explicitly instructed it to study step by step each
@@ -2188,7 +2188,7 @@ call site. In the following example, the body of \lstinline|f| is analyzed again
at each analysis of the body of the loop. The result of the analysis
is as precise as the result obtained for the example in section \ref{boucles}.
-\listinginput{1}{fonctions.c}
+\listinginput{1}{examples/fonctions.c}
Calls to variadic functions are handled by the \textsf{Variadic} plug-in, which
translates calls to variadic functions into semantically-equivalent calls,
@@ -2225,7 +2225,7 @@ assume that the actual entry point for the example of section
\ref{fonctions} is not the function \lstinline|main_1| but the following
\lstinline|main_main| function:
-\listinginput{17}{main.c}
+\listinginput{17}{examples/main.c}
If the user specifies the wrong
entry point \lstinline|main_1|, the plug-in will provide the
@@ -2479,7 +2479,7 @@ that the analyzed code fits in this hypothesis. On the following example,
it generates a proof obligation meaning that ``the comparison
on line 8 is safe only if \lstinline|p| is a valid address or if the base address
of \lstinline|p| is the same as that of \lstinline|&x|''.
-\listinginput{1}{bases.c}
+\listinginput{1}{examples/bases.c}
It is mandatory to check this proof obligation. When analyzing this
example, the analysis infers that the loop never terminates (because
@@ -2568,7 +2568,7 @@ real execution. Currently, \Eva{} is not designed to prove
the termination of loops or similar liveness properties.
For instance,
the following program does not terminate:
-\listinginput{1}{termination.c}
+\listinginput{1}{examples/termination.c}
If this program is analyzed
with the default options of \Eva{}, the analysis finds
that every time execution reaches the end of \lstinline|main|, the value
@@ -4233,7 +4233,7 @@ of this function. In the example below, the dependency of
\lstinline|double_assign| is \lstinline|a FROM c|.
The variable \lstinline|b| is not a functional input because the final value
of \lstinline|a| depends only on \lstinline|c|.
-\listinginput{1}{double_assign.c}
+\listinginput{1}{examples/double_assign.c}
The dependencies of a function may also be listed as \lstinline|NO EFFECTS|.
This means that the function has no effects when it terminates. There
@@ -4318,7 +4318,7 @@ are guaranteed to have been over-written when the function terminates;
the latter is a by-product of the computation of operational
inputs that someone may find useful someday.
-\listinginput{1}{op_inputs.c}
+\listinginput{1}{examples/op_inputs.c}
This example, when analyzed with the options \lstinline|-inout -lib-entry -main op|,
is found to have on termination the operational
@@ -4406,7 +4406,7 @@ ensure that the property $P$ holds.
Let us consider for instance the following function.
-\listinginput{1}{reduction.c}
+\listinginput{1}{examples/reduction.c}
\begin{shell}
frama-c -eva -eva-slevel 12 -lib-entry -main f reduction.c
@@ -4442,7 +4442,7 @@ in that point of the program.
This treatment often improves the precision of the analysis. It can be used with tautological assertions
to provide hints to the analyzer, as shown in the following example.
-\listinginput{1}{sq.c}
+\listinginput{1}{examples/sq.c}
\begin{shell}
frama-c -eva -eva-slevel 2 sq.c
@@ -4481,7 +4481,7 @@ not taken into account at all.
\smallskip
The two functions below illustrate both of these limitations:
-\listinginput{1}{annotations_2.c}
+\listinginput{1}{examples/annotations_2.c}
If the analyzer is launched with
options \lstinline|-lib-entry -main generalization|,
@@ -5003,7 +5003,7 @@ The implementation of these functions might change in future versions
of Frama-C, but their types and their behavior will stay the same.
Example of use of the functions introducing non-determinism:
-\listinginput{1}{nondet.c}
+\listinginput{1}{examples/nondet.c}
With the command below, the obtained result for
variable \lstinline|X| is \lstinline|[-45..150],0%3|.
@@ -5409,7 +5409,7 @@ time. For these reasons, \lstinline|-ulevel| is seldom used nowadays.
The answers to these questions are ``yes'' and ``yes''.
Consider the following example:
-\listinginput{1}{vraie_al.c}
+\listinginput{1}{examples/vraie_al.c}
When analyzing this example, \Eva{} does not emit an
alarm on line 6. This is perfectly correct, since no error occurs at
@@ -5440,7 +5440,7 @@ the case of a false alarm. Deciding whether the first alarm is a true
or a false one is the responsibility of the user.
This situation
happens in the following example:
-\listinginput{1}{false_al.c}
+\listinginput{1}{examples/false_al.c}
Analyzing this example with the default options produces:
\begin{logs}
diff --git a/doc/value/makefile b/doc/value/makefile
index 674a0cc5d30670a872aa9e1219635262c8e78fe3..e7799466cb4418291ff270fac8d4dffb0086d3d9 100644
--- a/doc/value/makefile
+++ b/doc/value/makefile
@@ -1,5 +1,3 @@
-GENERATED=main.aux main.cb main.cb2 main.log main.out main.toc main.pdf
-
all: main
.PHONY: main
@@ -10,7 +8,7 @@ include ../MakeLaTeXModern
OPENSOURCE?=yes
export OPENSOURCE
-main: ../../VERSION *.c
+main: ../../VERSION examples/**.c
$(MAKE) -C examples/parametrizing
$(MAKE) $(FRAMAC_MODERN)
latexmk -pdf main.tex
@@ -21,7 +19,7 @@ else
endif
clean:
- rm -f $(GENERATED)
+ latexmk -C -bibtex
install:
rm -f ../manuals/eva-manual.pdf
diff --git a/doc/value/revert_preview.scpt b/doc/value/revert_preview.scpt
deleted file mode 100644
index 4e7ef74055d16df432d23af15ccac2adbf239999..0000000000000000000000000000000000000000
--- a/doc/value/revert_preview.scpt
+++ /dev/null
@@ -1,26 +0,0 @@
- --- activate Preview
- tell application "Preview"
- activate
- end tell
-
- --- Interface with the document
- tell application "System Events"
- tell process "Preview"
- --- Select Revert from the File menu
- tell menu bar 1
- tell menu bar item "File"
- tell menu 1
- click menu item "Revert"
- end tell
- end tell
- end tell
-
- --- Restore the original page (assumes standard toolbar layout)
- --- Is there an easier way?
---- tell window 1
---- keystroke tab & tab & tab & return
---- keystroke tab & tab & tab & tab using {shift down}
---- end tell
- end tell
- end tell
-