diff --git a/ALL_VERSIONS b/ALL_VERSIONS
index d9447f7b7d320386cd109d9acaaefc53da5ca3c8..41c8714b5e8cec36bdab5450c57eb8db4568e653 100644
--- a/ALL_VERSIONS
+++ b/ALL_VERSIONS
@@ -1,5 +1,6 @@
Version number Date of release Notes
============== =============== =====
+19.0 (Potassium) 2019, June 21
18.0 (Argon) 2018, November 29
Chlorine-20180502 2018, July 06 Bug fixed
Chlorine-20180501 2018, June 01
diff --git a/Makefile.generating b/Makefile.generating
index 04faf2bbc7a06a9c5326c0fb07a415fda453dd1c..ea525bf3630c865e6385d89d634fe30127e3dc91 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -153,8 +153,8 @@ endif
ifeq ($(HAS_OCAML408),yes)
DYNLINK_INIT=fun () -> ()
FORMAT_STAG=stag
- FORMAT_STRING_OF_STAG=match s with\n\
- | Format.String_tag str -> str\n\
+ FORMAT_STRING_OF_STAG=match s with \
+ Format.String_tag str -> str \
| _ -> raise (Invalid_argument "unsupported tag extension")
FORMAT_STAG_OF_STRING=Format.String_tag s
else
diff --git a/VERSION b/VERSION
index e05f67667f953aef068e3ff9bf4a4244478e7463..0c48b6c985e328b88a009121a6e0431a102a7db0 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-19.0-beta2
\ No newline at end of file
+19.0
\ No newline at end of file
diff --git a/configure.in b/configure.in
index 1c508452c3e88478318f82fff46c8a61dbe09c0f..385594f9759b0f6de70d69d985667c1f633f8e5b 100644
--- a/configure.in
+++ b/configure.in
@@ -967,7 +967,7 @@ if test "$SOURCEVIEW_PATH" = ""; then
echo "Ocamlfind -> using $LABLGTK_PATH"
LABLGTKPATH_FOR_CONFIGURE=$LABLGTK_PATH
fi;
- SOURCEVIEW_PATH=$LABLGTK_PATH;
+ SOURCEVIEW_PATH=$LABLGTKPATH_FOR_CONFIGURE;
else
LABLGTK_VERSION=3
echo "ocamlfind -> using $LABLGTK_PATH"
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}
diff --git a/opam/opam b/opam/opam
index 7b2c44a9fa950c7f74182a16dd6bf4f04e6cd759..162d6fd2734d587766cf41b9165cfbd9323830bc 100644
--- a/opam/opam
+++ b/opam/opam
@@ -1,7 +1,7 @@
opam-version: "2.0"
name: "frama-c"
synopsis: "Platform dedicated to the analysis of source code written in C"
-version: "19.0.beta2"
+version: "19.0"
maintainer: "francois.bobot@cea.fr"
authors: [
"Michele Alberti"
@@ -94,17 +94,20 @@ depends: [
( ( "lablgtk" { >= "2.18.2" } & "conf-gnomecanvas" )
| ( "lablgtk3" { >= "3.0.beta4" & os!="macos" } & "lablgtk3-sourceview3" ))
"conf-gtksourceview"
- ( "alt-ergo-free" | "alt-ergo" )
+ ( "alt-ergo-free" | "alt-ergo" { <= "2.2.0" } )
"conf-graphviz" { post }
"yojson"
]
depopts: [
- "coq" { build }
- "why3" { build }
- "why3-coq" { build }
- "mlgmpidl" { build }
- "apron" { build }
+ # cannot use {build}: Frama-C must be recompiled when Coq and libraries changes.
+ # Coq: because .vo would would not be loadable by another version of Coq
+ # libraries: because we use dynamic linking
+ "coq"
+ "why3"
+ "why3-coq"
+ "mlgmpidl"
+ "apron"
]
conflicts: [
diff --git a/src/kernel_internals/runtime/config.mli b/src/kernel_internals/runtime/config.mli
index 80c125ae0c08c5d0a3955961112c8ab7235c4bd3..fb6d070c74c0f041e99aa5f94513fe84fb8d9833 100644
--- a/src/kernel_internals/runtime/config.mli
+++ b/src/kernel_internals/runtime/config.mli
@@ -36,11 +36,11 @@ val version_and_codename: string
val major_version: int
(** Frama-C major version number.
- @since Frama-C+dev *)
+ @since 19.0-Potassium *)
val minor_version: int
(** Frama-C minor version number.
- @since Frama-C+dev *)
+ @since 19.0-Potassium *)
val is_gui: bool ref
(** Is the Frama-C GUI running?
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 9ca6bee84604575fe2f429beada46f30681d215f..7e0addfa37b30314353f07196413221e3125885d 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1066,7 +1066,7 @@ and stmt = {
mutable sattr : attributes
(** Statement attributes.
- @since Frama-C+dev *)
+ @since 19.0-Potassium *)
}
(** Labels *)
diff --git a/src/kernel_services/ast_data/kernel_function.mli b/src/kernel_services/ast_data/kernel_function.mli
index dc999bb6dc809590ce5b9f4c0c9c638eaecbf75c..0dcbc8acb7307aaa3e1c0f79adec20665a386b87 100644
--- a/src/kernel_services/ast_data/kernel_function.mli
+++ b/src/kernel_services/ast_data/kernel_function.mli
@@ -113,7 +113,7 @@ val common_block: stmt -> stmt -> block
both [s1] and [s2], provided the statements belong to the same function.
raises a fatal error if this is not the case.
- @since Frama-C+dev
+ @since 19.0-Potassium
*)
val stmt_in_loop: t -> stmt -> bool
@@ -141,7 +141,7 @@ val var_is_in_scope: stmt -> varinfo -> bool
that on the contrary to {!Globals.Syntactic_search.find_in_scope}, the
variable is searched according to its [vid], not its [vorig_name].
- @since Frama-C+dev *)
+ @since 19.0-Potassium *)
val find_enclosing_stmt_in_block: block -> stmt -> stmt
(** [find_enclosing_stmt_in_block b s] returns the statements [s']
@@ -149,7 +149,7 @@ val find_enclosing_stmt_in_block: block -> stmt -> stmt
an inner block (recursively) containing [s].
@raise AbortFatal if [b] is not equal to [find_enclosing_block s]
- @since Frama-C+dev
+ @since 19.0-Potassium
*)
val is_between: block -> stmt -> stmt -> stmt -> bool
@@ -160,7 +160,7 @@ val is_between: block -> stmt -> stmt -> stmt -> bool
@raise AbortFatal if pre-conditions are not met.
- @since Frama-C+dev
+ @since 19.0-Potassium
*)
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index d951fa1afb61b2990baece699c57ff35cc83b462..8b91f7fde54b52978f527327f159800142371b7a 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -448,7 +448,7 @@ val ip_of_global_annotation_single:
val has_status: identified_property -> bool
(** Does the property has a logical status (which may be Never_tried)?
False for pragma, assumes clauses and some ACSL extensions.
- @since Frama-C+dev *)
+ @since 19.0-Potassium *)
val get_kinstr: identified_property -> kinstr
val get_kf: identified_property -> kernel_function option
@@ -467,7 +467,7 @@ val source: identified_property -> Filepath.position option
(**************************************************************************)
-(** @since Frama-C+dev deprecated old naming scheme,
+(** @since 19.0-Potassium deprecated old naming scheme,
to be removed in future versions. *)
module LegacyNames :
sig
@@ -485,12 +485,12 @@ sig
val get_prop_name_id: identified_property -> string
(** returns a unique name identifying the property.
This name is built from the basename of the property.
- @modify Frama-C+dev new naming scheme, Cf. LegacyNames
+ @modify 19.0-Potassium new naming scheme, Cf. LegacyNames
*)
val get_prop_basename: ?truncate:int -> identified_property -> string
(** returns the basename of the property.
- @modify Frama-C+dev additional truncation parameter
+ @modify 19.0-Potassium additional truncation parameter
*)
end
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index bcb8991186ad056f30b552187d9ab42c0e35fec8..bd9004a95867dd7da8ecc2ade9eb7c2ae8829970 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -538,12 +538,12 @@ val isCharArrayType: typ -> bool
val isIntegralType: typ -> bool
(** True if the argument is [_Bool]
- @since Frama-C+dev
+ @since 19.0-Potassium
*)
val isBoolType: typ -> bool
(** True if the argument is [_Bool] or [boolean].
- @since Frama-C+dev
+ @since 19.0-Potassium
*)
val isLogicPureBooleanType: logic_type -> bool
@@ -855,7 +855,7 @@ val isLogicNull: term -> bool
(** [no_op_coerce typ term] is [true] iff converting [term] to [typ] does
not modify its value.
- @since Frama-C+dev
+ @since 19.0-Potassium
*)
val no_op_coerce: logic_type -> term -> bool
@@ -2074,7 +2074,7 @@ val visitCilBlock: cilVisitor -> block -> block
and contain definitions of local variables that are not part of the block.
@since Phosphorus-20170501-beta1
- @modify Frama-C+dev: do not raise fatal as soon as the block has locals
+ @modify 19.0-Potassium: do not raise fatal as soon as the block has locals
*)
val transient_block: block -> block
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index f30df04280448362252376dfc6aa835029466b64..e6c6c5460f6373b9a5681550d8ec601875ac4e5d 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -176,7 +176,7 @@ type typing_context = {
@since Carbon-20101201
@modify Silicon-20161101 change type of the function
- @modify Frama-C+dev add [status] argument
+ @modify 19.0-Potassium add [status] argument
*)
val register_behavior_extension:
string -> bool ->
@@ -295,7 +295,7 @@ sig
@param explicit true if the cast is present in original source.
defaults to false
@since Nitrogen-20111001
- @modify Frama-C+dev introduces explicit param
+ @modify 19.0-Potassium introduces explicit param
*)
val mk_cast:
?explicit:bool -> Cil_types.term -> Cil_types.logic_type -> Cil_types.term
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index 1fdba6ce16dfa0177dea43c0bc00adb72f480b90..86d7bec02790d0ec2ced3af931ab3c239910cc0f 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -340,7 +340,7 @@ val mkdir : ?parents:bool -> string -> Unix.file_perm -> unit
user execution of the created directory. This will leave the filesystem
in a modified state before raising an exception.
@raise Unix.Unix_error if cannot create [name] or its parents.
- @since Frama-C+dev *)
+ @since 19.0-Potassium *)
val safe_at_exit : (unit -> unit) -> unit
(** Register function to call with [Pervasives.at_exit], but only
diff --git a/src/plugins/gui/gtk_helper.mli b/src/plugins/gui/gtk_helper.mli
index 776e4d3560d974bb684e74186bb8489875709025..6d9d605b34bf5dd4da7058b20f071f786cbb47f5 100644
--- a/src/plugins/gui/gtk_helper.mli
+++ b/src/plugins/gui/gtk_helper.mli
@@ -326,7 +326,7 @@ val source_files_chooser:
of the selected file. Replaces GToolbox.select_file that has not been
ported to lablgtk3.
- @since Frama-C+dev
+ @since 19.0-Potassium
*)
val select_file:
?title:string -> ?dir:(string ref)-> ?filename:string -> unit -> string option
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index c90573422be52a7c907c16cf8a120da6b736ec73..046d11b86db369105ea05b45ef3007157e2bddc8 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -25,29 +25,29 @@
Plugin WP 19.0 (Potassium)
##########################
- - Wp [2019/05/09] Fixes -wp-simplify-is-cint simplifier
- - Wp [2019/04/26] Now requires -warn-invalid-bool
- - Wp [2019/04/26] Removed option -wp-bool-range
- - Wp [2019/04/24] Support for Why3 1.* and Coq 8.{7-9}
- - Wp [2019/02/26] Support for @check ACSL annotations
- - WP [2018/02/16] Filter out some variables from separation
- - TIP [2018/02/15] Extend bitwise-eq auto-strategy on hypotheses
- - TIP [2018/02/15] Fix wrong reconciliation of sub-scripts during replay
- - Wp [2018/02/15] Better naming convention, consistent with report-classify
- - WP [2019/02/05] Auto filter properties with name "no_wp:"
- - Wp [2019/01/28] Now -wp-dynamic is set by default (annotation @calls)
- - Wp [2019/01/28] New floating-point model
- - Wp [2018/01/18] Auto-Search mode, see -wp-auto
- - TIP [2018/01/18] Auto-Search mode from the GUI
- - TIP [2018/01/18] New Strategies for bitwise and congruence operations
- - TIP [2017/12/17] Fix bug that makes the TIP wrongly reuse previous results
- - Wp [2017/12/17] Option -wp-print-separation changed into -wp-warn-separation
- - Wp [2017/12/17] Option -wp-unfold-assigns for proving assigns of aggregates field by field
- - TIP [2017/04/25] New tactical Congruence (divisions and products)
- - Qed [2017/10/30] Extends simplifications for lsl,lsr and div
- - Wp [2017/10/27] Fix soundness bug when assigning non-valid ranges
- - Qed [2017/10/27] New simplifications for validity and ranges
- - TIP [2017/10/27] New tacticals for validity and ranges
+- Wp [2019/05/09] Fixes -wp-simplify-is-cint simplifier
+- Wp [2019/04/26] Now requires -warn-invalid-bool
+- Wp [2019/04/26] Removed option -wp-bool-range
+- Wp [2019/04/24] Support for Why3 1.* and Coq 8.{7-9}
+- Wp [2019/02/26] Support for @check ACSL annotations
+- WP [2018/02/16] Filter out some variables from separation
+- TIP [2018/02/15] Extend bitwise-eq auto-strategy on hypotheses
+- TIP [2018/02/15] Fix wrong reconciliation of sub-scripts during replay
+- Wp [2018/02/15] Better naming convention, consistent with report-classify
+- WP [2019/02/05] Auto filter properties with name "no_wp:"
+- Wp [2019/01/28] Now -wp-dynamic is set by default (annotation @calls)
+- Wp [2019/01/28] New floating-point model
+- Wp [2018/01/18] Auto-Search mode, see -wp-auto
+- TIP [2018/01/18] Auto-Search mode from the GUI
+- TIP [2018/01/18] New Strategies for bitwise and congruence operations
+- TIP [2017/12/17] Fix bug that makes the TIP wrongly reuse previous results
+- Wp [2017/12/17] Option -wp-print-separation changed into -wp-warn-separation
+- Wp [2017/12/17] Option -wp-unfold-assigns for proving assigns of aggregates field by field
+- TIP [2017/04/25] New tactical Congruence (divisions and products)
+- Qed [2017/10/30] Extends simplifications for lsl,lsr and div
+- Wp [2017/10/27] Fix soundness bug when assigning non-valid ranges
+- Qed [2017/10/27] New simplifications for validity and ranges
+- TIP [2017/10/27] New tacticals for validity and ranges
######################
Plugin WP 18.0 (Argon)
@@ -66,21 +66,21 @@ Plugin WP 18.0 (Argon)
Plugin WP Sulfur-20171101
#########################
- - Wp [2017/10/18] Support for LoopCurrent and LoopEntry
- - TIP [2017/04/25] Options -wp-time-{extra|margin} for more stability
- -* Gui [2017/04/25] Fixed bug when running prover from the TIP
- - Wp [2017/04/25] Improved model and simplifications of logical shifts
- - Wp [2017/04/25] New simplification logic functions (-wp-reduce)
- - Wp [2017/04/25] New simplification of unused variables (-wp-parasite)
- - Wp [2017/04/25] New simplification for ground terms (-wp-ground)
- - Wp [2017/04/25] Option -wp-prenex to normalize nested binders
- - Wp [2017/04/25] Option -wp-overflows to add explicit assumptions
- - TIP [2017/04/25] New tactical Overflow (to cope with modulus)
- - TIP [2017/04/25] New tactical Ratio (divisions and products)
- - TIP [2017/04/25] New tactical Bitwised, BitRange and Shift
- - TIP [2017/04/25] New tactical Rewrite (two apply equalities)
- - Wp [2017/03/12] Reduction of equalities with logic functions
- - Wp [2017/03/12] More simplifications wrt integer domains
+- Wp [2017/10/18] Support for LoopCurrent and LoopEntry
+- TIP [2017/04/25] Options -wp-time-{extra|margin} for more stability
+-* Gui [2017/04/25] Fixed bug when running prover from the TIP
+- Wp [2017/04/25] Improved model and simplifications of logical shifts
+- Wp [2017/04/25] New simplification logic functions (-wp-reduce)
+- Wp [2017/04/25] New simplification of unused variables (-wp-parasite)
+- Wp [2017/04/25] New simplification for ground terms (-wp-ground)
+- Wp [2017/04/25] Option -wp-prenex to normalize nested binders
+- Wp [2017/04/25] Option -wp-overflows to add explicit assumptions
+- TIP [2017/04/25] New tactical Overflow (to cope with modulus)
+- TIP [2017/04/25] New tactical Ratio (divisions and products)
+- TIP [2017/04/25] New tactical Bitwised, BitRange and Shift
+- TIP [2017/04/25] New tactical Rewrite (two apply equalities)
+- Wp [2017/03/12] Reduction of equalities with logic functions
+- Wp [2017/03/12] More simplifications wrt integer domains
###########################
Plugin WP Chlorine-20180501