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/context-depth.1.log b/doc/value/examples/parametrizing/context-depth.1.log
index 3f4497589cbc27fa521ad5ceb14ae2f1b9a7ea87..add271dee9176cff36bc65c00afff99ec9293cb6 100644
--- a/doc/value/examples/parametrizing/context-depth.1.log
+++ b/doc/value/examples/parametrizing/context-depth.1.log
@@ -77,3 +77,14 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 1 statements reached (out of 1): 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/context-depth.2.log b/doc/value/examples/parametrizing/context-depth.2.log
index aa40ac4e166ab6994dcc729eda29c971fbc26b9c..872bda66319fccd4ef428f54fa1cfb2b7b4769a0 100644
--- a/doc/value/examples/parametrizing/context-depth.2.log
+++ b/doc/value/examples/parametrizing/context-depth.2.log
@@ -18,3 +18,14 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 1 statements reached (out of 1): 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/context-depth.3.log b/doc/value/examples/parametrizing/context-depth.3.log
index 796a0b6e08f3e0952ff512a2f7bad3f25e026eda..b907017b2956d3f0ce7778a3ea9d5f7ed02c5529 100644
--- a/doc/value/examples/parametrizing/context-depth.3.log
+++ b/doc/value/examples/parametrizing/context-depth.3.log
@@ -13,3 +13,14 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 1 statements reached (out of 1): 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/context-width.log b/doc/value/examples/parametrizing/context-width.log
index 9edcb21f15572a56426ca9304f0d6863bad55b3e..c586ab0c3b57b65077801e1f27d8eb031532480b 100644
--- a/doc/value/examples/parametrizing/context-width.log
+++ b/doc/value/examples/parametrizing/context-width.log
@@ -18,3 +18,14 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 2 statements reached (out of 2): 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/global-initial-values.log b/doc/value/examples/parametrizing/global-initial-values.log
index f8a0ada3b0ebfb0280ec51512ac60ffbef5d0556..105b797c406f2d4a8edf73d82bd3963c5b8b8aa2 100644
--- a/doc/value/examples/parametrizing/global-initial-values.log
+++ b/doc/value/examples/parametrizing/global-initial-values.log
@@ -11,3 +11,14 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 1 statements reached (out of 1): 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/ilevel.1.log b/doc/value/examples/parametrizing/ilevel.1.log
index c24bbec5ea55aafd4dd4ec002f046c27471d5397..de93eb9610ea6147566d6e9338bebe74f34ef9e4 100644
--- a/doc/value/examples/parametrizing/ilevel.1.log
+++ b/doc/value/examples/parametrizing/ilevel.1.log
@@ -21,3 +21,17 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
__retres ∈ [2..31]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 5 statements reached (out of 5): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 1 valid 0 unknown 0 invalid 1 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/ilevel.2.log b/doc/value/examples/parametrizing/ilevel.2.log
index 49de84286e0f1c25406f1f449e8623c106750a82..8cef794e55af22fb5509812b86a3028f29cc12c6 100644
--- a/doc/value/examples/parametrizing/ilevel.2.log
+++ b/doc/value/examples/parametrizing/ilevel.2.log
@@ -21,3 +21,17 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
__retres ∈ {2; 3; 5; 7; 11; 13; 17; 19; 23; 27; 29; 31}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 5 statements reached (out of 5): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 1 valid 0 unknown 0 invalid 1 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/loop-unroll-const.c b/doc/value/examples/parametrizing/loop-unroll-const.c
new file mode 100644
index 0000000000000000000000000000000000000000..58211a63ed4c9ea947771b863c9489941549e173
--- /dev/null
+++ b/doc/value/examples/parametrizing/loop-unroll-const.c
@@ -0,0 +1,12 @@
+#define NROWS 10
+void main(void)
+{
+ int a[NROWS][20] = {0};
+ //@ loop unroll NROWS;
+ for (int i = 0; i < 10; i++) {
+ //@ loop unroll (10+10);
+ for (int j = 0; j < 20; j++) {
+ a[i][j] += i + j;
+ }
+ }
+}
diff --git a/doc/value/examples/parametrizing/loop-unroll-const.log b/doc/value/examples/parametrizing/loop-unroll-const.log
new file mode 100644
index 0000000000000000000000000000000000000000..4e1d575004122744df61587538cab466b0959b29
--- /dev/null
+++ b/doc/value/examples/parametrizing/loop-unroll-const.log
@@ -0,0 +1,222 @@
+[kernel] Parsing loop-unroll-const.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] 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:
+ a[0][0] ∈ {0}
+ [0][1] ∈ {1}
+ [0][2] ∈ {2}
+ [0][3] ∈ {3}
+ [0][4] ∈ {4}
+ [0][5] ∈ {5}
+ [0][6] ∈ {6}
+ [0][7] ∈ {7}
+ [0][8] ∈ {8}
+ [0][9] ∈ {9}
+ [0][10] ∈ {10}
+ [0][11] ∈ {11}
+ [0][12] ∈ {12}
+ [0][13] ∈ {13}
+ [0][14] ∈ {14}
+ [0][15] ∈ {15}
+ [0][16] ∈ {16}
+ [0][17] ∈ {17}
+ [0][18] ∈ {18}
+ [0][19] ∈ {19}
+ [1][0] ∈ {1}
+ [1][1] ∈ {2}
+ [1][2] ∈ {3}
+ [1][3] ∈ {4}
+ [1][4] ∈ {5}
+ [1][5] ∈ {6}
+ [1][6] ∈ {7}
+ [1][7] ∈ {8}
+ [1][8] ∈ {9}
+ [1][9] ∈ {10}
+ [1][10] ∈ {11}
+ [1][11] ∈ {12}
+ [1][12] ∈ {13}
+ [1][13] ∈ {14}
+ [1][14] ∈ {15}
+ [1][15] ∈ {16}
+ [1][16] ∈ {17}
+ [1][17] ∈ {18}
+ [1][18] ∈ {19}
+ [1][19] ∈ {20}
+ [2][0] ∈ {2}
+ [2][1] ∈ {3}
+ [2][2] ∈ {4}
+ [2][3] ∈ {5}
+ [2][4] ∈ {6}
+ [2][5] ∈ {7}
+ [2][6] ∈ {8}
+ [2][7] ∈ {9}
+ [2][8] ∈ {10}
+ [2][9] ∈ {11}
+ [2][10] ∈ {12}
+ [2][11] ∈ {13}
+ [2][12] ∈ {14}
+ [2][13] ∈ {15}
+ [2][14] ∈ {16}
+ [2][15] ∈ {17}
+ [2][16] ∈ {18}
+ [2][17] ∈ {19}
+ [2][18] ∈ {20}
+ [2][19] ∈ {21}
+ [3][0] ∈ {3}
+ [3][1] ∈ {4}
+ [3][2] ∈ {5}
+ [3][3] ∈ {6}
+ [3][4] ∈ {7}
+ [3][5] ∈ {8}
+ [3][6] ∈ {9}
+ [3][7] ∈ {10}
+ [3][8] ∈ {11}
+ [3][9] ∈ {12}
+ [3][10] ∈ {13}
+ [3][11] ∈ {14}
+ [3][12] ∈ {15}
+ [3][13] ∈ {16}
+ [3][14] ∈ {17}
+ [3][15] ∈ {18}
+ [3][16] ∈ {19}
+ [3][17] ∈ {20}
+ [3][18] ∈ {21}
+ [3][19] ∈ {22}
+ [4][0] ∈ {4}
+ [4][1] ∈ {5}
+ [4][2] ∈ {6}
+ [4][3] ∈ {7}
+ [4][4] ∈ {8}
+ [4][5] ∈ {9}
+ [4][6] ∈ {10}
+ [4][7] ∈ {11}
+ [4][8] ∈ {12}
+ [4][9] ∈ {13}
+ [4][10] ∈ {14}
+ [4][11] ∈ {15}
+ [4][12] ∈ {16}
+ [4][13] ∈ {17}
+ [4][14] ∈ {18}
+ [4][15] ∈ {19}
+ [4][16] ∈ {20}
+ [4][17] ∈ {21}
+ [4][18] ∈ {22}
+ [4][19] ∈ {23}
+ [5][0] ∈ {5}
+ [5][1] ∈ {6}
+ [5][2] ∈ {7}
+ [5][3] ∈ {8}
+ [5][4] ∈ {9}
+ [5][5] ∈ {10}
+ [5][6] ∈ {11}
+ [5][7] ∈ {12}
+ [5][8] ∈ {13}
+ [5][9] ∈ {14}
+ [5][10] ∈ {15}
+ [5][11] ∈ {16}
+ [5][12] ∈ {17}
+ [5][13] ∈ {18}
+ [5][14] ∈ {19}
+ [5][15] ∈ {20}
+ [5][16] ∈ {21}
+ [5][17] ∈ {22}
+ [5][18] ∈ {23}
+ [5][19] ∈ {24}
+ [6][0] ∈ {6}
+ [6][1] ∈ {7}
+ [6][2] ∈ {8}
+ [6][3] ∈ {9}
+ [6][4] ∈ {10}
+ [6][5] ∈ {11}
+ [6][6] ∈ {12}
+ [6][7] ∈ {13}
+ [6][8] ∈ {14}
+ [6][9] ∈ {15}
+ [6][10] ∈ {16}
+ [6][11] ∈ {17}
+ [6][12] ∈ {18}
+ [6][13] ∈ {19}
+ [6][14] ∈ {20}
+ [6][15] ∈ {21}
+ [6][16] ∈ {22}
+ [6][17] ∈ {23}
+ [6][18] ∈ {24}
+ [6][19] ∈ {25}
+ [7][0] ∈ {7}
+ [7][1] ∈ {8}
+ [7][2] ∈ {9}
+ [7][3] ∈ {10}
+ [7][4] ∈ {11}
+ [7][5] ∈ {12}
+ [7][6] ∈ {13}
+ [7][7] ∈ {14}
+ [7][8] ∈ {15}
+ [7][9] ∈ {16}
+ [7][10] ∈ {17}
+ [7][11] ∈ {18}
+ [7][12] ∈ {19}
+ [7][13] ∈ {20}
+ [7][14] ∈ {21}
+ [7][15] ∈ {22}
+ [7][16] ∈ {23}
+ [7][17] ∈ {24}
+ [7][18] ∈ {25}
+ [7][19] ∈ {26}
+ [8][0] ∈ {8}
+ [8][1] ∈ {9}
+ [8][2] ∈ {10}
+ [8][3] ∈ {11}
+ [8][4] ∈ {12}
+ [8][5] ∈ {13}
+ [8][6] ∈ {14}
+ [8][7] ∈ {15}
+ [8][8] ∈ {16}
+ [8][9] ∈ {17}
+ [8][10] ∈ {18}
+ [8][11] ∈ {19}
+ [8][12] ∈ {20}
+ [8][13] ∈ {21}
+ [8][14] ∈ {22}
+ [8][15] ∈ {23}
+ [8][16] ∈ {24}
+ [8][17] ∈ {25}
+ [8][18] ∈ {26}
+ [8][19] ∈ {27}
+ [9][0] ∈ {9}
+ [9][1] ∈ {10}
+ [9][2] ∈ {11}
+ [9][3] ∈ {12}
+ [9][4] ∈ {13}
+ [9][5] ∈ {14}
+ [9][6] ∈ {15}
+ [9][7] ∈ {16}
+ [9][8] ∈ {17}
+ [9][9] ∈ {18}
+ [9][10] ∈ {19}
+ [9][11] ∈ {20}
+ [9][12] ∈ {21}
+ [9][13] ∈ {22}
+ [9][14] ∈ {23}
+ [9][15] ∈ {24}
+ [9][16] ∈ {25}
+ [9][17] ∈ {26}
+ [9][18] ∈ {27}
+ [9][19] ∈ {28}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 16 statements reached (out of 16): 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/loop-unroll-insuf.c b/doc/value/examples/parametrizing/loop-unroll-insuf.c
new file mode 100644
index 0000000000000000000000000000000000000000..f977bfe31f574efdb9f5a13ca0b3b2f9f14f06c2
--- /dev/null
+++ b/doc/value/examples/parametrizing/loop-unroll-insuf.c
@@ -0,0 +1,6 @@
+void main()
+{
+ //@ loop unroll 20; // should be 21
+ for (int i = 0 ; i <= 20 ; i ++) {
+ }
+}
\ No newline at end of file
diff --git a/doc/value/examples/parametrizing/loop-unroll-insuf.log b/doc/value/examples/parametrizing/loop-unroll-insuf.log
new file mode 100644
index 0000000000000000000000000000000000000000..6478cadfa123687fb56495c0684d673d42724499
--- /dev/null
+++ b/doc/value/examples/parametrizing/loop-unroll-insuf.log
@@ -0,0 +1,23 @@
+[kernel] Parsing loop-unroll-insuf.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: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:
+ i ∈ {21}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 6 statements reached (out of 6): 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/loop-unroll-nested.c b/doc/value/examples/parametrizing/loop-unroll-nested.c
new file mode 100644
index 0000000000000000000000000000000000000000..62a61e7ad9e6836bcfec553030ef97988abf2119
--- /dev/null
+++ b/doc/value/examples/parametrizing/loop-unroll-nested.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};
+void main(void)
+{
+ int S = 0;
+ //@ loop unroll 3;
+ for (int i = 0 ; i < 3 ; 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
new file mode 100644
index 0000000000000000000000000000000000000000..d126c7d04246aba236742011e2b0e36f8f4d23e0
--- /dev/null
+++ b/doc/value/examples/parametrizing/loop-unroll-nested.log
@@ -0,0 +1,35 @@
+[kernel] Parsing loop-unroll-nested.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] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ S ∈ {45}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 16 statements reached (out of 16): 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/makefile b/doc/value/examples/parametrizing/makefile
index 5c550ea370ed05402aca8edee17c7fbcb15cdd96..e2be7e2a93403c33937fceab58817dc1557785be 100644
--- a/doc/value/examples/parametrizing/makefile
+++ b/doc/value/examples/parametrizing/makefile
@@ -14,7 +14,12 @@ TARGETS = \
nor.1.log \
nor.2.log \
ilevel.1.log \
- ilevel.2.log
+ ilevel.2.log \
+ loop-unroll-const.log \
+ loop-unroll-nested.log \
+ loop-unroll-insuf.log \
+ split-array.log \
+ split-fabs.log
.SECONDEXPANSION:
.PHONY: all clean
@@ -35,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/nor.1.log b/doc/value/examples/parametrizing/nor.1.log
index d9202d664a9fe97e59eaea38a4e1256f1bb8fbd9..292dfde5dd433ad2514ddf17d6ff9051303a918c 100644
--- a/doc/value/examples/parametrizing/nor.1.log
+++ b/doc/value/examples/parametrizing/nor.1.log
@@ -5,26 +5,26 @@
[eva:initial-state] Values of globals at initialization
t[0..1999] ∈ {0}
i ∈ {0}
-[eva] Semantic level unrolling superposing up to 100 states
-[eva] Semantic level unrolling superposing up to 200 states
-[eva] Semantic level unrolling superposing up to 300 states
-[eva] Semantic level unrolling superposing up to 400 states
-[eva] Semantic level unrolling superposing up to 500 states
-[eva] Semantic level unrolling superposing up to 600 states
-[eva] Semantic level unrolling superposing up to 700 states
-[eva] Semantic level unrolling superposing up to 800 states
-[eva] Semantic level unrolling superposing up to 900 states
-[eva] Semantic level unrolling superposing up to 1000 states
-[eva] Semantic level unrolling superposing up to 1100 states
-[eva] Semantic level unrolling superposing up to 1200 states
-[eva] Semantic level unrolling superposing up to 1300 states
-[eva] Semantic level unrolling superposing up to 1400 states
-[eva] Semantic level unrolling superposing up to 1500 states
-[eva] Semantic level unrolling superposing up to 1600 states
-[eva] Semantic level unrolling superposing up to 1700 states
-[eva] Semantic level unrolling superposing up to 1800 states
-[eva] Semantic level unrolling superposing up to 1900 states
-[eva] Semantic level unrolling superposing up to 2000 states
+[eva] nor.c:5: Trace partitioning superposing up to 100 states
+[eva] nor.c:5: Trace partitioning superposing up to 200 states
+[eva] nor.c:5: Trace partitioning superposing up to 300 states
+[eva] nor.c:5: Trace partitioning superposing up to 400 states
+[eva] nor.c:5: Trace partitioning superposing up to 500 states
+[eva] nor.c:5: Trace partitioning superposing up to 600 states
+[eva] nor.c:5: Trace partitioning superposing up to 700 states
+[eva] nor.c:5: Trace partitioning superposing up to 800 states
+[eva] nor.c:5: Trace partitioning superposing up to 900 states
+[eva] nor.c:5: Trace partitioning superposing up to 1000 states
+[eva] nor.c:5: Trace partitioning superposing up to 1100 states
+[eva] nor.c:5: Trace partitioning superposing up to 1200 states
+[eva] nor.c:5: Trace partitioning superposing up to 1300 states
+[eva] nor.c:5: Trace partitioning superposing up to 1400 states
+[eva] nor.c:5: Trace partitioning superposing up to 1500 states
+[eva] nor.c:5: Trace partitioning superposing up to 1600 states
+[eva] nor.c:5: Trace partitioning superposing up to 1700 states
+[eva] nor.c:5: Trace partitioning superposing up to 1800 states
+[eva] nor.c:5: Trace partitioning superposing up to 1900 states
+[eva] nor.c:5: Trace partitioning superposing up to 2000 states
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function irrelevant_function:
@@ -4032,5 +4032,16 @@
[1999] ∈ {1999}
i ∈ {2000}
__retres ∈ {143}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 10 statements reached (out of 10): 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.
+ ----------------------------------------------------------------------------
-user time: 0.61s
+user time: 7.67s
diff --git a/doc/value/examples/parametrizing/nor.2.log b/doc/value/examples/parametrizing/nor.2.log
index d79d6ad6a29371e5d6322a3cb2cb57eade5733ba..de472ed593d9225272ff7c5ed569b91e6601cd43 100644
--- a/doc/value/examples/parametrizing/nor.2.log
+++ b/doc/value/examples/parametrizing/nor.2.log
@@ -5,26 +5,26 @@
[eva:initial-state] Values of globals at initialization
t[0..1999] ∈ {0}
i ∈ {0}
-[eva] Semantic level unrolling superposing up to 100 states
-[eva] Semantic level unrolling superposing up to 200 states
-[eva] Semantic level unrolling superposing up to 300 states
-[eva] Semantic level unrolling superposing up to 400 states
-[eva] Semantic level unrolling superposing up to 500 states
-[eva] Semantic level unrolling superposing up to 600 states
-[eva] Semantic level unrolling superposing up to 700 states
-[eva] Semantic level unrolling superposing up to 800 states
-[eva] Semantic level unrolling superposing up to 900 states
-[eva] Semantic level unrolling superposing up to 1000 states
-[eva] Semantic level unrolling superposing up to 1100 states
-[eva] Semantic level unrolling superposing up to 1200 states
-[eva] Semantic level unrolling superposing up to 1300 states
-[eva] Semantic level unrolling superposing up to 1400 states
-[eva] Semantic level unrolling superposing up to 1500 states
-[eva] Semantic level unrolling superposing up to 1600 states
-[eva] Semantic level unrolling superposing up to 1700 states
-[eva] Semantic level unrolling superposing up to 1800 states
-[eva] Semantic level unrolling superposing up to 1900 states
-[eva] Semantic level unrolling superposing up to 2000 states
+[eva] nor.c:5: Trace partitioning superposing up to 100 states
+[eva] nor.c:5: Trace partitioning superposing up to 200 states
+[eva] nor.c:5: Trace partitioning superposing up to 300 states
+[eva] nor.c:5: Trace partitioning superposing up to 400 states
+[eva] nor.c:5: Trace partitioning superposing up to 500 states
+[eva] nor.c:5: Trace partitioning superposing up to 600 states
+[eva] nor.c:5: Trace partitioning superposing up to 700 states
+[eva] nor.c:5: Trace partitioning superposing up to 800 states
+[eva] nor.c:5: Trace partitioning superposing up to 900 states
+[eva] nor.c:5: Trace partitioning superposing up to 1000 states
+[eva] nor.c:5: Trace partitioning superposing up to 1100 states
+[eva] nor.c:5: Trace partitioning superposing up to 1200 states
+[eva] nor.c:5: Trace partitioning superposing up to 1300 states
+[eva] nor.c:5: Trace partitioning superposing up to 1400 states
+[eva] nor.c:5: Trace partitioning superposing up to 1500 states
+[eva] nor.c:5: Trace partitioning superposing up to 1600 states
+[eva] nor.c:5: Trace partitioning superposing up to 1700 states
+[eva] nor.c:5: Trace partitioning superposing up to 1800 states
+[eva] nor.c:5: Trace partitioning superposing up to 1900 states
+[eva] nor.c:5: Trace partitioning superposing up to 2000 states
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
@@ -2031,5 +2031,16 @@ Cannot filter: dumping raw memory (including unchanged variables)
[1999] ∈ {1999}
i ∈ {2000}
__retres ∈ {143}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 10 statements reached (out of 10): 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.
+ ----------------------------------------------------------------------------
-user time: 0.26s
+user time: 3.11s
diff --git a/doc/value/examples/parametrizing/out-of-bound.log b/doc/value/examples/parametrizing/out-of-bound.log
index 06f21f7998e676d93d8c108dbcd2b48ef71f4447..365e3edd937c7a33c60cbe1bb5381abda8849cb9 100644
--- a/doc/value/examples/parametrizing/out-of-bound.log
+++ b/doc/value/examples/parametrizing/out-of-bound.log
@@ -11,3 +11,16 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
NON TERMINATING FUNCTION
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 2): 50% coverage.
+ In this function, 1 statements reached (out of 2): 50% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 access out of bounds index
+ 1 of them is a sure alarm (invalid status).
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/simple-main.log b/doc/value/examples/parametrizing/simple-main.log
index d7defe1645a43850de824800f0e19a9bb6aff94f..63b112ec39394c71a88c5f29323ccf83fe27c333 100644
--- a/doc/value/examples/parametrizing/simple-main.log
+++ b/doc/value/examples/parametrizing/simple-main.log
@@ -19,3 +19,14 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
__retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 3 statements reached (out of 3): 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/slevel.1.log b/doc/value/examples/parametrizing/slevel.1.log
index ca308071d5497e913e04fc07d678bf47f1c09be3..7fab16b9dd70afcef09736b1028774c06db758fd 100644
--- a/doc/value/examples/parametrizing/slevel.1.log
+++ b/doc/value/examples/parametrizing/slevel.1.log
@@ -12,3 +12,14 @@
i ∈ {5}
j ∈ {10}
t[0..4][0..9] ∈ {1}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 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/examples/parametrizing/slevel.2.log b/doc/value/examples/parametrizing/slevel.2.log
index 9459da3c9930632a9ddf3d8c636f893133700702..cc1474f37db4dac630cbd75f34b91f3d24380ef9 100644
--- a/doc/value/examples/parametrizing/slevel.2.log
+++ b/doc/value/examples/parametrizing/slevel.2.log
@@ -14,3 +14,14 @@
j ∈ {10}
t{[0..1][0..9]; [2][0..5]} ∈ {1}
{[2][6..9]; [3..4][0..9]} ∈ {0; 1}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 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/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/examples/parametrizing/widen-hints.log b/doc/value/examples/parametrizing/widen-hints.log
index 9e760a40d3385119f17618e60c584b5e1c63d888..b02525597d9e147f58fc3de93f49ce02e709d7d3 100644
--- a/doc/value/examples/parametrizing/widen-hints.log
+++ b/doc/value/examples/parametrizing/widen-hints.log
@@ -12,3 +12,14 @@
i ∈ {13}
j ∈ [0..55]
n ∈ {13}
+[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/main.tex b/doc/value/main.tex
index a541d32a9a709ff3c1bd5e5deb9856acf1a749ae..018e077c1f4c7502f5ceb740e2a088ea05df347e 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.
@@ -3308,29 +3309,35 @@ iteration, avoiding merging states from different iterations.
This leads to increased cost in terms of analysis, but usually the cost
increase is worth the improvement in precision.
-Such annotations must be placed before just before the loop (i.e. before the
+Such annotations must be placed just before the loop (i.e. before the
\lstinline|while|, \lstinline|for| or \lstinline|do| introducing the loop),
and one annotation is required per loop, including nested ones. For instance:
-\begin{lstlisting}
-#define NROWS 10
-void main() {
- int a[NROWS][20] = {0};
- //@ loop unroll NROWS;
- for (int i = 0; i < 10; i++) {
- //@ loop unroll (10+10);
- for (int j = 0; j < 20; j++) {
- a[i][j] += i + j;
- }
- }
-}
-\end{lstlisting}
+\lstinputlisting{examples/parametrizing/loop-unroll-const.c}
-Note that constants obtained via \lstinline|#define| macros can be used in
-annotations, as well as constant expressions. The annotations above will ensure
+The annotations above will ensure
that \Eva{} will unroll the loops and keep the analysis precise; otherwise,
the array access \lstinline|a[i][j]| might generate alarms due to imprecisions.
+The \lstinline|loop unroll| parameter can be any C expression evaluated to a
+single integer value by \Eva{} each time the analysis reaches the loop.
+Otherwise, the annotation is ignored and a warning is issued.
+Constants obtained via \lstinline|#define| macros, variables which always have
+a unique value and arithmetic operators are suitable.
+For expressions that have several possible values,
+the acceptability of the annotation depends on the precision of the analyzer.
+Note that there are interesting cases of non-constant expressions for
+unrolling annotations. The example below shows a function with two nested loops.
+
+\lstinputlisting{examples/parametrizing/loop-unroll-nested.c}
+
+The number of iterations of the outer loop is constant while the number of
+iterations of the inner loop depends on the current iteration of the outer
+one. As we have instructed \Eva{} to unroll the outer loop, it evaluates the
+parameter \lstinline|sizes[i]| to a single possible integer for each iteration
+of the outer loop, and thus the inner loop annotation is accepted. In this
+example, it is also possible to use an upper bound like $4$.
+
The unrolling mechanism is independent of \lstinline|-eva-slevel|
(see next subsection): annotated loops are always unrolled at least the specified
number of times. If the loop has not been entirely unrolled, however,
@@ -3340,17 +3347,12 @@ While it is sometimes useful to unroll only the first iterations, the usual
objective is full unrolling; for this reason, the user is informed whenever
the specified unrolling value is insufficient to unroll the loop entirely:
-\begin{lstlisting}
-void main() {
- //@ loop unroll 20; // should be 21
- for (int i = 0 ; i <= 20 ; i ++) {
- }
-}
-\end{lstlisting}
+\begin{minipage}{\linewidth}% prevents page break in listing
+\lstinputlisting{examples/parametrizing/loop-unroll-insuf.c}
+\end{minipage}
-\begin{lstlisting}
-[eva:loop-unroll] insuf-loop.c:3: loop not completely unrolled
-\end{lstlisting}
+\lstinputlisting[linerange={7-7}]
+ {examples/parametrizing/loop-unroll-insuf.log}
The message can be deactived via \lstinline|-eva-warn-key loop-unroll=inactive|.
@@ -3710,6 +3712,119 @@ line~7, by an invariant, that remains to be proven.
%% less precisely.
+\section{Improving precision with case-based reasoning}
+\label{trace-partitioning}
+
+Some formal proofs about programs require to use \emph{case-based reasoning}.
+\Eva{} can perform such reasonings through \emph{trace partitioning}
+\cite{trace-partitioning} techniques, which can be enabled globally or
+by specific annotations. It is important to note that, whatever the method used,
+a partitioning (and thus the case-based reasoning) currently 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 by an \lstinline|if-then-else| statement or a
+\lstinline|switch| not far above, even if these blocks are already closed
+at the point we need the case-based reasoning. Unless enough
+\lstinline|slevel| is available, the cases of a conditional structure are
+approximated together as soon as the analyzer leaves the block. However, \Eva{}
+can delay this approximation until after the statement where the case-based
+reasoning is needed.
+
+The global command-line parameter \lstinline|-eva-partition-history <n>|
+delays the approximation for all conditional structures of the whole
+program. The parameter \lstinline|<n>| controls the delay:
+it represents the number of junction points for which the incoming
+paths (the cases) are kept separated. At a given point, \Eva{} is then able to
+reason by cases on the \lstinline|<n>| last \lstinline|if-then-else| statements
+closed before.
+A value of $1$ means that \Eva{} will reason by
+case on the previous \lstinline|if-then-else|, until another one is closed.
+
+This option has a very high cost on the analysis, theoretically doubling the
+analysis time for each increment of its parameter $n$.
+The cost can even be higher on \lstinline|switch| statements.
+However, it can remove false alarms in a fully automatic way. Thus,
+the trade off might often be worth trying.
+
+In practice, \lstinline|-eva-partition-history 1| seems to be sufficient in
+most cases, and a greater value is rarely needed.
+
+
+\subsection{Value partitioning}
+
+A case-based reasoning on the possible values of an expression can be forced
+inside a function by using \lstinline|split| annotations. These annotations
+must be given an expression which values correspond to the cases that need to be
+enumerated. The example below shows an usage of this annotation.
+
+\lstinputlisting{examples/parametrizing/split-array.c}
+
+The \lstinline|split| instructs \Eva{} to enumerate all the possible
+values of \lstinline|i| and to continue the analysis separately for
+each of these values. Thereafter, the value of \lstinline|i| is always
+evaluated by \Eva{} as a singleton in each case, which 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 values instead
+of an imprecise interval.
+
+\lstinputlisting[linerange={25-26}]
+ {examples/parametrizing/split-array.log}
+
+A \lstinline|split| annotation can be used on any expression that evaluates to a
+{\it small} number of integer values. In particular, the expression can be a C
+comparison like in the following example.
+
+\lstinputlisting{examples/parametrizing/split-fabs.c}
+
+This example requires the equality domain (enabled with option
+\lstinline|-eva-equality-domain|, see section \ref{sec:symbolic-equalities}) to
+be analyzed precisely, 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 before the call to \lstinline|fabs|
+allows \Eva{} to reason by case and to infer the relevant equality in each case.
+
+This example also illustrates the use of a \lstinline|merge| annotation, which
+ends the case-based reasoning started by a previous \lstinline|split| annotation
+with the exact same expression.
+The use of \lstinline|merge| annotations is not mandatory, but they allow the
+user to mitigate the cost of \lstinline|split| annotations.
+
+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 four limitations to the value partitioning:
+
+\begin{enumerate}
+\item Splits can only be performed on integer expressions. Pointers and
+ floating-point values are not supported yet.
+\item The expression on which the split is done must evaluate to a small set of
+ integer values, in order to limit the cost of the partitioning and ensure the
+ termination of the analysis. If the number of possible values infered for the
+ expression exceeds a defined limit, \Eva{} cancels the split and emits a
+ warning. The limit is 100 by default and can be changed with option
+ \lstinline|-eva-split-limit <n>|.
+\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| annotations use 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 case-based reasoning
+ is controlled accross the whole program.
+\item When the expression is complex, the ability of \Eva{} to reason
+ precisely by cases depends on the enabled abstract domains (see section
+ \ref{sec:eva}) and their capability to learn from the value of the expression.
+ If \Eva{} detects that the expression is too complex for the split to be useful,
+ it will cancel the split and warn the user.
+\end{enumerate}
+
+
\section{Controlling approximations}
\label{controlling-approximations}