diff --git a/doc/value/biblio.bib b/doc/value/biblio.bib
index afdbbf9218d7537cce903dde676973f4b123dbb2..d284b32a7af847422825480741062ef8d5d0dc05 100644
--- a/doc/value/biblio.bib
+++ b/doc/value/biblio.bib
@@ -115,3 +115,22 @@
biburl = {https://dblp.org/rec/bib/conf/sas/2018},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
+
+
+@article{trace-partitioning,
+ author = {Rival, Xavier and Mauborgne, Laurent},
+ title = {The Trace Partitioning Abstract Domain},
+ journal = {ACM Trans. Program. Lang. Syst.},
+ issue_date = {August 2007},
+ volume = {29},
+ number = {5},
+ month = aug,
+ year = {2007},
+ issn = {0164-0925},
+ articleno = {26},
+ url = {http://doi.acm.org/10.1145/1275497.1275501},
+ doi = {10.1145/1275497.1275501},
+ acmid = {1275501},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}
\ No newline at end of file
diff --git a/doc/value/examples/parametrizing/loop-unroll-const.c b/doc/value/examples/parametrizing/loop-unroll-const.c
index dad47c0b39970db177d8da0990f340547869be78..58211a63ed4c9ea947771b863c9489941549e173 100644
--- a/doc/value/examples/parametrizing/loop-unroll-const.c
+++ b/doc/value/examples/parametrizing/loop-unroll-const.c
@@ -1,5 +1,6 @@
#define NROWS 10
-void main(void) {
+void main(void)
+{
int a[NROWS][20] = {0};
//@ loop unroll NROWS;
for (int i = 0; i < 10; i++) {
diff --git a/doc/value/examples/parametrizing/loop-unroll-const.log b/doc/value/examples/parametrizing/loop-unroll-const.log
index 9071ef760702f7c63c8f525a0d9db24cc1a7fcec..4e1d575004122744df61587538cab466b0959b29 100644
--- a/doc/value/examples/parametrizing/loop-unroll-const.log
+++ b/doc/value/examples/parametrizing/loop-unroll-const.log
@@ -4,8 +4,8 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] loop-unroll-const.c:7: Trace partitioning superposing up to 100 states
-[eva] loop-unroll-const.c:7: Trace partitioning superposing up to 200 states
+[eva] loop-unroll-const.c:8: Trace partitioning superposing up to 100 states
+[eva] loop-unroll-const.c:8: Trace partitioning superposing up to 200 states
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
diff --git a/doc/value/examples/parametrizing/loop-unroll-insuf.c b/doc/value/examples/parametrizing/loop-unroll-insuf.c
index 5058c9d40465278fcd2384a68c20b8ac5145ec31..f977bfe31f574efdb9f5a13ca0b3b2f9f14f06c2 100644
--- a/doc/value/examples/parametrizing/loop-unroll-insuf.c
+++ b/doc/value/examples/parametrizing/loop-unroll-insuf.c
@@ -1,4 +1,5 @@
-void main() {
+void main()
+{
//@ loop unroll 20; // should be 21
for (int i = 0 ; i <= 20 ; i ++) {
}
diff --git a/doc/value/examples/parametrizing/loop-unroll-insuf.log b/doc/value/examples/parametrizing/loop-unroll-insuf.log
index 7527748a566d26ddc05c101e38be93f36658b2bf..6478cadfa123687fb56495c0684d673d42724499 100644
--- a/doc/value/examples/parametrizing/loop-unroll-insuf.log
+++ b/doc/value/examples/parametrizing/loop-unroll-insuf.log
@@ -4,8 +4,8 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:loop-unroll] loop-unroll-insuf.c:3: loop not completely unrolled
-[eva] loop-unroll-insuf.c:3: starting to merge loop iterations
+[eva:loop-unroll] loop-unroll-insuf.c:4: loop not completely unrolled
+[eva] loop-unroll-insuf.c:4: starting to merge loop iterations
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
diff --git a/doc/value/examples/parametrizing/loop-unroll-nested.c b/doc/value/examples/parametrizing/loop-unroll-nested.c
index 7205a6d088a5e2cc53311f6117d8da4de7c159a9..62a61e7ad9e6836bcfec553030ef97988abf2119 100644
--- a/doc/value/examples/parametrizing/loop-unroll-nested.c
+++ b/doc/value/examples/parametrizing/loop-unroll-nested.c
@@ -1,11 +1,12 @@
int t1[] = {1, 2, 3}, t2[] = {4, 5}, t3[] = {6, 7, 8, 9};
int *t[] = {t1, t2, t3};
int sizes[] = {3, 2, 4};
-void main(void) {
+void main(void)
+{
int S = 0;
- // loop unroll 3;
+ //@ loop unroll 3;
for (int i = 0 ; i < 3 ; i++) {
- // loop unroll sizes[i];
+ //@ loop unroll sizes[i];
for (int j = 0 ; j < sizes[i] ; j++) {
S += t[i][j];
}
diff --git a/doc/value/examples/parametrizing/loop-unroll-nested.log b/doc/value/examples/parametrizing/loop-unroll-nested.log
index 5ff936dc9484d1016ed2a8f7f0350ff2732fa92d..d126c7d04246aba236742011e2b0e36f8f4d23e0 100644
--- a/doc/value/examples/parametrizing/loop-unroll-nested.log
+++ b/doc/value/examples/parametrizing/loop-unroll-nested.log
@@ -18,16 +18,10 @@
sizes[0] ∈ {3}
[1] ∈ {2}
[2] ∈ {4}
-[eva] loop-unroll-nested.c:9: starting to merge loop iterations
-[eva:alarm] loop-unroll-nested.c:10: Warning:
- signed overflow. assert S + *(t[i] + j) ≤ 2147483647;
-[eva] loop-unroll-nested.c:7: starting to merge loop iterations
-[eva:alarm] loop-unroll-nested.c:10: Warning:
- out of bounds read. assert \valid_read(t[i] + j);
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
- S ∈ [0..2147483647]
+ S ∈ {45}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
1 function analyzed (out of 1): 100% coverage.
@@ -35,9 +29,7 @@
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
- 2 alarms generated by the analysis:
- 1 invalid memory access
- 1 integer overflow
+ 0 alarms generated by the analysis.
----------------------------------------------------------------------------
No logical properties have been reached by the analysis.
----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/makefile b/doc/value/examples/parametrizing/makefile
index 74f6d633930c2a34e7dc807cd156f262ef801a0c..e2be7e2a93403c33937fceab58817dc1557785be 100644
--- a/doc/value/examples/parametrizing/makefile
+++ b/doc/value/examples/parametrizing/makefile
@@ -17,7 +17,9 @@ TARGETS = \
ilevel.2.log \
loop-unroll-const.log \
loop-unroll-nested.log \
- loop-unroll-insuf.log
+ loop-unroll-insuf.log \
+ split-array.log \
+ split-fabs.log
.SECONDEXPANSION:
.PHONY: all clean
@@ -38,6 +40,7 @@ context-depth.3.log: FCFLAGS += -context-width 1 -context-depth 1 -context-valid
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
diff --git a/doc/value/examples/parametrizing/split-array.c b/doc/value/examples/parametrizing/split-array.c
new file mode 100644
index 0000000000000000000000000000000000000000..66c9037a253b117befc28cc21ac3cc5f86929128
--- /dev/null
+++ b/doc/value/examples/parametrizing/split-array.c
@@ -0,0 +1,14 @@
+int t1[] = {1, 2, 3}, t2[] = {4, 5}, t3[] = {6, 7, 8, 9};
+int *t[] = {t1, t2, t3};
+int sizes[] = {3, 2, 4};
+/*@ requires 0 <= i < 3; */
+int main(int i)
+{
+ int S = 0;
+ //@ split i;
+ //@ loop unroll sizes[i];
+ for (int j = 0 ; j < sizes[i] ; j++)
+ S += t[i][j];
+
+ return S;
+}
diff --git a/doc/value/examples/parametrizing/split-array.log b/doc/value/examples/parametrizing/split-array.log
new file mode 100644
index 0000000000000000000000000000000000000000..53a9ddd932748d851458163c1c4c9e1f4d461370
--- /dev/null
+++ b/doc/value/examples/parametrizing/split-array.log
@@ -0,0 +1,37 @@
+[kernel] Parsing split-array.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ t1[0] ∈ {1}
+ [1] ∈ {2}
+ [2] ∈ {3}
+ t2[0] ∈ {4}
+ [1] ∈ {5}
+ t3[0] ∈ {6}
+ [1] ∈ {7}
+ [2] ∈ {8}
+ [3] ∈ {9}
+ t[0] ∈ {{ &t1[0] }}
+ [1] ∈ {{ &t2[0] }}
+ [2] ∈ {{ &t3[0] }}
+ sizes[0] ∈ {3}
+ [1] ∈ {2}
+ [2] ∈ {4}
+[eva:alarm] split-array.c:4: Warning:
+ function main: precondition got status unknown.
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ S ∈ {6; 9; 30}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 9 statements reached (out of 9): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/split-fabs.c b/doc/value/examples/parametrizing/split-fabs.c
new file mode 100644
index 0000000000000000000000000000000000000000..92b25ba9fcb2dd4513927136f07bee1c96e52169
--- /dev/null
+++ b/doc/value/examples/parametrizing/split-fabs.c
@@ -0,0 +1,13 @@
+double fabs(double x)
+{
+ return x < 0.0 ? -x : x;
+}
+
+double main(double y)
+{
+ //@ split y < 0.0;
+ if (fabs(y) > 1.0)
+ y = y < 0 ? -1.0 : 1.0;
+ //@ merge y < 0.0;
+ return y;
+}
diff --git a/doc/value/examples/parametrizing/split-fabs.log b/doc/value/examples/parametrizing/split-fabs.log
new file mode 100644
index 0000000000000000000000000000000000000000..130b40492718c8d7d8fe39fff39e56c159223f92
--- /dev/null
+++ b/doc/value/examples/parametrizing/split-fabs.log
@@ -0,0 +1,23 @@
+[kernel] Parsing split-fabs.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function fabs:
+
+[eva:final-states] Values at end of function main:
+ y ∈ [-1. .. 1.]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 12 statements reached (out of 12): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/main.tex b/doc/value/main.tex
index 62fb14dd0f03505ef305f334c8781dc024a46d4c..d9e502263777808b0cd5635c41e1b98737f6887f 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -2658,6 +2658,7 @@ Section \ref{command-line} presents the general usage options of \Eva{} in the
command-line.
The options described in section \ref{context} are correctness options,
while the remaining sections (\ref{boucles-traitement},
+\ref{trace-partitioning},
\ref{controlling-approximations} and \ref{sec:eva}) deal with performance
tuning options. Section \ref{nonterm} presents a derived analysis to
obtain information about non-termination.
@@ -3711,6 +3712,118 @@ line~7, by an invariant, that remains to be proven.
%% less precisely.
+\section{Improving precision with reasoning by case}
+\label{trace-partitioning}
+
+Some formal proofs about programs require to use \emph{reasoning by cases}. \Eva can
+perform such reasonings through the use of the \emph{Trace Partitioning}
+\cite{trace-partitioning} techniques. These can be enabled manually or
+automatically. It is important to note that, whatever the method used, the
+partitioning and thus the reasoning by case stops at the end of a function
+and can only be extended past the function return if there is enough
+\lstinline|slevel| in the calling function.
+
+
+\subsection{Automatic partitioning on conditional structures}
+
+It sometimes happens that the cases we want to reason on are exactly the
+cases distinguished in the program in an \lstinline|if-then-else| or a
+\lstinline|switch| not far above. even if these blocks are already closed
+at the point we need the reasoning by cases. Unless enough
+\lstinline|slevel| is available, the cases of a conditional structures are
+approximated together as soon as the analyzer leaves the block. \Eva can delay
+this approximation until after the statement where the reasoning
+by cases is needed.
+
+The global command-line parameter \lstinline|-eva-partition-history <n>|
+will delay the approximation for all conditional structures of the whole
+program. It takes a parameter \lstinline|<n>| which allow to control the delay.
+It represents the number of junction points for which we keep the incoming
+path (the cases) separated. A value of $1$ means that \Eva will reason by
+case on the previous \lstinline|if-then-else| until another
+\lstinline|if-then-else| is closed.
+
+This option has a very high cost on the analysis, theoretically increasing the
+analysis time by 2 for $n = 1$, and doubling each time $n$ is increased by $1$.
+The cost can even be higher if there are \lstinline|switch| instructions in the
+program. However, it can remove false alarms in a fully automatic way. Thus,
+the trade off might often be worth trying.
+
+Choosing a value for \lstinline|<n>| strictly greater than 1 is often not
+needed.
+
+
+\subsection{Manual partitioning on values}
+
+The reasoning by case can be forced inside a function by using \lstinline|split|
+annotations. These annotations must be given an expression which values
+correspond to the cases being enumerated. The example below show a usage
+of this annotation.
+
+\lstinputlisting{examples/parametrizing/split-array.c}
+
+The \lstinline|split| requires that the analyzer enumerate all the 3 possible
+values for \lstinline|i| and conduct a specialized analysis of the function for
+each of these values. Thereafter, the value of \lstinline|i| is always
+evalutated by \Eva{} as a singleton and it enables the use of a
+\lstinline|loop unroll| annotation on \lstinline|i|. This way, the result of
+the function can be exactly computed as the set of three possible value instead
+of an imprecise interval.
+
+\lstinputlisting[linerange={25-26}]
+ {examples/parametrizing/split-array.log}
+
+The \lstinline|split| can be any expression that evaluate to a {\it small}
+number of integer values. In particular, it can be C comparisons like in
+the following example.
+
+\lstinputlisting{examples/parametrizing/split-fabs.c}
+
+To be analyzed properly, the equality domain must be activated with the option
+\lstinline|-eva-equality-domain| (see section \ref{sec:symbolic-equalities})
+as we need the equality relations between the input and the output of the
+function \lstinline|fabs|, i.e. the relations \lstinline|x == \result| or
+\lstinline|x == -\result|. Then, the \lstinline|split| annotation placed before
+the call to \lstinline|fabs| allows us to reason by case and infer the relevant
+equality in each case.
+
+Note in the previous example the use of \lstinline|merge| annotation. These
+annotations ends the reasoning by cases and must use the exact same expression
+as a previous \lstinline|split|. In this example, the \lstinline|merge|
+annotation is not needed as the partitioning will be ended at the end of the
+function anyway. The use of \lstinline|merge| annotations is not mandatory,
+and are these annotations exists only to allow the user to mitigate the cost of
+the reasoning by cases.
+
+Alternatively to annotations, it is possible to use the command-line to
+reason by case during the whole analysis. The command line parameter
+\lstinline|-eva-partition-value <V>| forces the analyzer to reason at all times
+on single values of the global variable \lstinline|<V>|.
+
+There are three limitations to partitioning on values.
+
+\begin{enumerate}
+\item While the number of simultaneous splits (whether local with annotations
+ or global through command line) is not bounded, there can be only one split
+ per expression. If two \lstinline|split| annotation uses the same expression,
+ only the latest one encountered on the path will be kept. Although it is a
+ limitation, it can be used to define strategies where a reasoning by case is
+ controlled accross the whole program.
+\item The expression on which the split is done must evaluate to a bounded set
+ of values. Otherwise, the analysis would not be guaranteed to terminate. The
+ analysis must be precise enough in order to prove the boundedness. When \Eva{}
+ fails to prove that the number of possible values is lower than a defined limit,
+ either because the set is unbounded or because it failed to prove it,
+ it will raise a warning and cancel the split. The limit is arbitrary and
+ can be set with the option \lstinline|-eva-split-limit <n>|.
+\item When the expression is complex, the ability of \Eva{} to reason
+ precisely by cases depends on the activated abstract domains (see section
+ \ref{sec:eva}) and their capability to learn from the expression. \Eva{} will
+ try to detect this and will cancel the split and warn the user when it is
+ not useful.
+\end{enumerate}
+
+
\section{Controlling approximations}
\label{controlling-approximations}