diff options
| author | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-04-30 17:19:08 +0200 |
|---|---|---|
| committer | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-04-30 17:19:08 +0200 |
| commit | bcde99fbe99174a094f38fdda70ad69d65a423f4 (patch) | |
| tree | 21e16494aba19c4a63d55eba877abfe7fe5d8e80 /tests | |
| download | SemVerif-Projet-bcde99fbe99174a094f38fdda70ad69d65a423f4.tar.gz SemVerif-Projet-bcde99fbe99174a094f38fdda70ad69d65a423f4.zip | |
Fist commit (WIP)
Diffstat (limited to 'tests')
304 files changed, 4383 insertions, 0 deletions
diff --git a/tests/README.txt b/tests/README.txt new file mode 100644 index 0000000..ff2a94c --- /dev/null +++ b/tests/README.txt @@ -0,0 +1,32 @@ +The sources/ directory contains a set of small program examples to test your +analyzer. + +The files are ordered by increasing complexity and language features. +They are classified into categories according to the file name prefix, +as follow: +- 00*: variable declarations, initialization with a constant +- 01*: printing, local declarations +- 02*: assignment, arithmetic operators +- 03*: if-then-else, comparisons and boolean operators +- 04*: assertions +- 05*: loops +- 06*: realistic examples mixing all of the above + +The results/ directory gives the output of the analysis using our +reference analyzer, with the constant, the interval, and the polyhedra +domains. +All the analyses are preformed using a loop unrolling of 3 and a widening +delay of 3. +Our analyzer outputs a line for each print instruction and for each assertion +failure, as well as the abstract environment when the program stops. +Note that, due to loop unrolling, a print or assert statement may be executed +more than once. Note also that, during fixpoint computation, the output of +print and assert statements is disabled; it is re-enabled only after the +fixpoint is reached, so that we do not print any information about the +iterates (which may not be invariants). + +For each source file and each domain (constants, intervals, polyhedra), we +provide the file output by the reference analyzer. +We also provide for each domain a summary file (named all.*.txt) that contains +each file followed by the analysis result, which may be more convenient to +read. diff --git a/tests/results/0000_noinit_var.constants.txt b/tests/results/0000_noinit_var.constants.txt new file mode 100644 index 0000000..1e125b7 --- /dev/null +++ b/tests/results/0000_noinit_var.constants.txt @@ -0,0 +1 @@ +Output: [ x in top ] diff --git a/tests/results/0000_noinit_var.intervals.txt b/tests/results/0000_noinit_var.intervals.txt new file mode 100644 index 0000000..eda51d2 --- /dev/null +++ b/tests/results/0000_noinit_var.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [-oo;+oo] ] diff --git a/tests/results/0000_noinit_var.polyhedra.txt b/tests/results/0000_noinit_var.polyhedra.txt new file mode 100644 index 0000000..f62b6cf --- /dev/null +++ b/tests/results/0000_noinit_var.polyhedra.txt @@ -0,0 +1 @@ +Output: top diff --git a/tests/results/0001_noinit_2var.constants.txt b/tests/results/0001_noinit_2var.constants.txt new file mode 100644 index 0000000..b7ada66 --- /dev/null +++ b/tests/results/0001_noinit_2var.constants.txt @@ -0,0 +1 @@ +Output: [ x in top, y in top ] diff --git a/tests/results/0001_noinit_2var.intervals.txt b/tests/results/0001_noinit_2var.intervals.txt new file mode 100644 index 0000000..f1b9aa5 --- /dev/null +++ b/tests/results/0001_noinit_2var.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [-oo;+oo], y in [-oo;+oo] ] diff --git a/tests/results/0001_noinit_2var.polyhedra.txt b/tests/results/0001_noinit_2var.polyhedra.txt new file mode 100644 index 0000000..f62b6cf --- /dev/null +++ b/tests/results/0001_noinit_2var.polyhedra.txt @@ -0,0 +1 @@ +Output: top diff --git a/tests/results/0002_init_var.constants.txt b/tests/results/0002_init_var.constants.txt new file mode 100644 index 0000000..6423d75 --- /dev/null +++ b/tests/results/0002_init_var.constants.txt @@ -0,0 +1 @@ +Output: [ x in {0} ] diff --git a/tests/results/0002_init_var.intervals.txt b/tests/results/0002_init_var.intervals.txt new file mode 100644 index 0000000..9fe0945 --- /dev/null +++ b/tests/results/0002_init_var.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [0;0] ] diff --git a/tests/results/0002_init_var.polyhedra.txt b/tests/results/0002_init_var.polyhedra.txt new file mode 100644 index 0000000..072e333 --- /dev/null +++ b/tests/results/0002_init_var.polyhedra.txt @@ -0,0 +1 @@ +Output: [|x=0|] diff --git a/tests/results/0003_init_2var.constants.txt b/tests/results/0003_init_2var.constants.txt new file mode 100644 index 0000000..9e88fcd --- /dev/null +++ b/tests/results/0003_init_2var.constants.txt @@ -0,0 +1 @@ +Output: [ x in {0}, y in {1} ] diff --git a/tests/results/0003_init_2var.intervals.txt b/tests/results/0003_init_2var.intervals.txt new file mode 100644 index 0000000..dd131bf --- /dev/null +++ b/tests/results/0003_init_2var.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [0;0], y in [1;1] ] diff --git a/tests/results/0003_init_2var.polyhedra.txt b/tests/results/0003_init_2var.polyhedra.txt new file mode 100644 index 0000000..efeddf5 --- /dev/null +++ b/tests/results/0003_init_2var.polyhedra.txt @@ -0,0 +1 @@ +Output: [|y-1=0; x=0|] diff --git a/tests/results/0004_init_2var2.constants.txt b/tests/results/0004_init_2var2.constants.txt new file mode 100644 index 0000000..91cb6ba --- /dev/null +++ b/tests/results/0004_init_2var2.constants.txt @@ -0,0 +1 @@ +Output: [ x in {9}, y in {12} ] diff --git a/tests/results/0004_init_2var2.intervals.txt b/tests/results/0004_init_2var2.intervals.txt new file mode 100644 index 0000000..709f31a --- /dev/null +++ b/tests/results/0004_init_2var2.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [9;9], y in [12;12] ] diff --git a/tests/results/0004_init_2var2.polyhedra.txt b/tests/results/0004_init_2var2.polyhedra.txt new file mode 100644 index 0000000..5b868c5 --- /dev/null +++ b/tests/results/0004_init_2var2.polyhedra.txt @@ -0,0 +1 @@ +Output: [|y-12=0; x-9=0|] diff --git a/tests/results/0100_print_var.constants.txt b/tests/results/0100_print_var.constants.txt new file mode 100644 index 0000000..7fd6b1c --- /dev/null +++ b/tests/results/0100_print_var.constants.txt @@ -0,0 +1,2 @@ +sources/0100_print_var.c:2.0-9: [ x in {2} ] +Output: [ x in {2} ] diff --git a/tests/results/0100_print_var.intervals.txt b/tests/results/0100_print_var.intervals.txt new file mode 100644 index 0000000..2fa1f97 --- /dev/null +++ b/tests/results/0100_print_var.intervals.txt @@ -0,0 +1,2 @@ +sources/0100_print_var.c:2.0-9: [ x in [2;2] ] +Output: [ x in [2;2] ] diff --git a/tests/results/0100_print_var.polyhedra.txt b/tests/results/0100_print_var.polyhedra.txt new file mode 100644 index 0000000..a0e67dd --- /dev/null +++ b/tests/results/0100_print_var.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0100_print_var.c:2.0-9: [|x-2=0|] +Output: [|x-2=0|] diff --git a/tests/results/0101_print_2var.constants.txt b/tests/results/0101_print_2var.constants.txt new file mode 100644 index 0000000..3a18b6c --- /dev/null +++ b/tests/results/0101_print_2var.constants.txt @@ -0,0 +1,2 @@ +sources/0101_print_2var.c:3.0-9: [ y in {15} ] +Output: [ x in {3}, y in {15} ] diff --git a/tests/results/0101_print_2var.intervals.txt b/tests/results/0101_print_2var.intervals.txt new file mode 100644 index 0000000..3a748f7 --- /dev/null +++ b/tests/results/0101_print_2var.intervals.txt @@ -0,0 +1,2 @@ +sources/0101_print_2var.c:3.0-9: [ y in [15;15] ] +Output: [ x in [3;3], y in [15;15] ] diff --git a/tests/results/0101_print_2var.polyhedra.txt b/tests/results/0101_print_2var.polyhedra.txt new file mode 100644 index 0000000..8d5d333 --- /dev/null +++ b/tests/results/0101_print_2var.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0101_print_2var.c:3.0-9: [|y-15=0|] +Output: [|y-15=0; x-3=0|] diff --git a/tests/results/0102_print_3var.constants.txt b/tests/results/0102_print_3var.constants.txt new file mode 100644 index 0000000..46882af --- /dev/null +++ b/tests/results/0102_print_3var.constants.txt @@ -0,0 +1,2 @@ +sources/0102_print_3var.c:4.0-11: [ z in {99}, x in {3} ] +Output: [ x in {3}, y in {15}, z in {99} ] diff --git a/tests/results/0102_print_3var.intervals.txt b/tests/results/0102_print_3var.intervals.txt new file mode 100644 index 0000000..1ec6fc8 --- /dev/null +++ b/tests/results/0102_print_3var.intervals.txt @@ -0,0 +1,2 @@ +sources/0102_print_3var.c:4.0-11: [ z in [99;99], x in [3;3] ] +Output: [ x in [3;3], y in [15;15], z in [99;99] ] diff --git a/tests/results/0102_print_3var.polyhedra.txt b/tests/results/0102_print_3var.polyhedra.txt new file mode 100644 index 0000000..c7ec366 --- /dev/null +++ b/tests/results/0102_print_3var.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0102_print_3var.c:4.0-11: [|z-99=0; x-3=0|] +Output: [|z-99=0; y-15=0; x-3=0|] diff --git a/tests/results/0103_local.constants.txt b/tests/results/0103_local.constants.txt new file mode 100644 index 0000000..5383bb9 --- /dev/null +++ b/tests/results/0103_local.constants.txt @@ -0,0 +1,2 @@ +sources/0103_local.c:4.2-5.0: [ x in {12}, y in {9} ] +Output: [ x in {12} ] diff --git a/tests/results/0103_local.intervals.txt b/tests/results/0103_local.intervals.txt new file mode 100644 index 0000000..360baa1 --- /dev/null +++ b/tests/results/0103_local.intervals.txt @@ -0,0 +1,2 @@ +sources/0103_local.c:4.2-5.0: [ x in [12;12], y in [9;9] ] +Output: [ x in [12;12] ] diff --git a/tests/results/0103_local.polyhedra.txt b/tests/results/0103_local.polyhedra.txt new file mode 100644 index 0000000..7a39013 --- /dev/null +++ b/tests/results/0103_local.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0103_local.c:4.2-5.0: [|y-9=0; x-12=0|] +Output: [|x-12=0|] diff --git a/tests/results/0200_assign_cst.constants.txt b/tests/results/0200_assign_cst.constants.txt new file mode 100644 index 0000000..479ad69 --- /dev/null +++ b/tests/results/0200_assign_cst.constants.txt @@ -0,0 +1,4 @@ +sources/0200_assign_cst.c:2.0-9: [ x in top ] +sources/0200_assign_cst.c:4.0-9: [ x in {12} ] +sources/0200_assign_cst.c:6.0-9: [ x in {15} ] +Output: [ x in {15} ] diff --git a/tests/results/0200_assign_cst.intervals.txt b/tests/results/0200_assign_cst.intervals.txt new file mode 100644 index 0000000..ed4ccb7 --- /dev/null +++ b/tests/results/0200_assign_cst.intervals.txt @@ -0,0 +1,4 @@ +sources/0200_assign_cst.c:2.0-9: [ x in [-oo;+oo] ] +sources/0200_assign_cst.c:4.0-9: [ x in [12;12] ] +sources/0200_assign_cst.c:6.0-9: [ x in [15;15] ] +Output: [ x in [15;15] ] diff --git a/tests/results/0200_assign_cst.polyhedra.txt b/tests/results/0200_assign_cst.polyhedra.txt new file mode 100644 index 0000000..1761595 --- /dev/null +++ b/tests/results/0200_assign_cst.polyhedra.txt @@ -0,0 +1,4 @@ +sources/0200_assign_cst.c:2.0-9: top +sources/0200_assign_cst.c:4.0-9: [|x-12=0|] +sources/0200_assign_cst.c:6.0-9: [|x-15=0|] +Output: [|x-15=0|] diff --git a/tests/results/0201_assign_cst2.constants.txt b/tests/results/0201_assign_cst2.constants.txt new file mode 100644 index 0000000..bf39084 --- /dev/null +++ b/tests/results/0201_assign_cst2.constants.txt @@ -0,0 +1,4 @@ +sources/0201_assign_cst2.c:2.0-11: [ x in top, y in top ] +sources/0201_assign_cst2.c:4.0-11: [ x in {12}, y in top ] +sources/0201_assign_cst2.c:7.0-11: [ x in {99}, y in {15} ] +Output: [ x in {99}, y in {15} ] diff --git a/tests/results/0201_assign_cst2.intervals.txt b/tests/results/0201_assign_cst2.intervals.txt new file mode 100644 index 0000000..5c3c77e --- /dev/null +++ b/tests/results/0201_assign_cst2.intervals.txt @@ -0,0 +1,4 @@ +sources/0201_assign_cst2.c:2.0-11: [ x in [-oo;+oo], y in [-oo;+oo] ] +sources/0201_assign_cst2.c:4.0-11: [ x in [12;12], y in [-oo;+oo] ] +sources/0201_assign_cst2.c:7.0-11: [ x in [99;99], y in [15;15] ] +Output: [ x in [99;99], y in [15;15] ] diff --git a/tests/results/0201_assign_cst2.polyhedra.txt b/tests/results/0201_assign_cst2.polyhedra.txt new file mode 100644 index 0000000..59df732 --- /dev/null +++ b/tests/results/0201_assign_cst2.polyhedra.txt @@ -0,0 +1,4 @@ +sources/0201_assign_cst2.c:2.0-11: top +sources/0201_assign_cst2.c:4.0-11: [|x-12=0|] +sources/0201_assign_cst2.c:7.0-11: [|y-15=0; x-99=0|] +Output: [|y-15=0; x-99=0|] diff --git a/tests/results/0202_assign_expr.constants.txt b/tests/results/0202_assign_expr.constants.txt new file mode 100644 index 0000000..c9ec364 --- /dev/null +++ b/tests/results/0202_assign_expr.constants.txt @@ -0,0 +1 @@ +Output: [ x in {4} ] diff --git a/tests/results/0202_assign_expr.intervals.txt b/tests/results/0202_assign_expr.intervals.txt new file mode 100644 index 0000000..da16d45 --- /dev/null +++ b/tests/results/0202_assign_expr.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [4;4] ] diff --git a/tests/results/0202_assign_expr.polyhedra.txt b/tests/results/0202_assign_expr.polyhedra.txt new file mode 100644 index 0000000..d9a3c72 --- /dev/null +++ b/tests/results/0202_assign_expr.polyhedra.txt @@ -0,0 +1 @@ +Output: [|x-4=0|] diff --git a/tests/results/0203_assign_expr2.constants.txt b/tests/results/0203_assign_expr2.constants.txt new file mode 100644 index 0000000..5bb2601 --- /dev/null +++ b/tests/results/0203_assign_expr2.constants.txt @@ -0,0 +1,2 @@ +sources/0203_assign_expr2.c:5.0-9: [ x in {30} ] +Output: [ x in {30}, y in {16} ] diff --git a/tests/results/0203_assign_expr2.intervals.txt b/tests/results/0203_assign_expr2.intervals.txt new file mode 100644 index 0000000..26e14b0 --- /dev/null +++ b/tests/results/0203_assign_expr2.intervals.txt @@ -0,0 +1,2 @@ +sources/0203_assign_expr2.c:5.0-9: [ x in [30;30] ] +Output: [ x in [30;30], y in [16;16] ] diff --git a/tests/results/0203_assign_expr2.polyhedra.txt b/tests/results/0203_assign_expr2.polyhedra.txt new file mode 100644 index 0000000..089a14e --- /dev/null +++ b/tests/results/0203_assign_expr2.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0203_assign_expr2.c:5.0-9: [|x-30=0|] +Output: [|y-16=0; x-30=0|] diff --git a/tests/results/0204_assign_rand.constants.txt b/tests/results/0204_assign_rand.constants.txt new file mode 100644 index 0000000..79463fd --- /dev/null +++ b/tests/results/0204_assign_rand.constants.txt @@ -0,0 +1,2 @@ +sources/0204_assign_rand.c:3.0-9: [ x in top ] +Output: [ x in top ] diff --git a/tests/results/0204_assign_rand.intervals.txt b/tests/results/0204_assign_rand.intervals.txt new file mode 100644 index 0000000..6ff24c2 --- /dev/null +++ b/tests/results/0204_assign_rand.intervals.txt @@ -0,0 +1,2 @@ +sources/0204_assign_rand.c:3.0-9: [ x in [1;99] ] +Output: [ x in [1;99] ] diff --git a/tests/results/0204_assign_rand.polyhedra.txt b/tests/results/0204_assign_rand.polyhedra.txt new file mode 100644 index 0000000..b32fd5e --- /dev/null +++ b/tests/results/0204_assign_rand.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0204_assign_rand.c:3.0-9: [|-x+99>=0; x-1>=0|] +Output: [|-x+99>=0; x-1>=0|] diff --git a/tests/results/0205_assign_rand2.constants.txt b/tests/results/0205_assign_rand2.constants.txt new file mode 100644 index 0000000..d907e00 --- /dev/null +++ b/tests/results/0205_assign_rand2.constants.txt @@ -0,0 +1,2 @@ +sources/0205_assign_rand2.c:3.0-9: bottom +Output: bottom diff --git a/tests/results/0205_assign_rand2.intervals.txt b/tests/results/0205_assign_rand2.intervals.txt new file mode 100644 index 0000000..d907e00 --- /dev/null +++ b/tests/results/0205_assign_rand2.intervals.txt @@ -0,0 +1,2 @@ +sources/0205_assign_rand2.c:3.0-9: bottom +Output: bottom diff --git a/tests/results/0205_assign_rand2.polyhedra.txt b/tests/results/0205_assign_rand2.polyhedra.txt new file mode 100644 index 0000000..d907e00 --- /dev/null +++ b/tests/results/0205_assign_rand2.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0205_assign_rand2.c:3.0-9: bottom +Output: bottom diff --git a/tests/results/0206_assign_add.constants.txt b/tests/results/0206_assign_add.constants.txt new file mode 100644 index 0000000..f03759a --- /dev/null +++ b/tests/results/0206_assign_add.constants.txt @@ -0,0 +1 @@ +Output: [ x in {7} ] diff --git a/tests/results/0206_assign_add.intervals.txt b/tests/results/0206_assign_add.intervals.txt new file mode 100644 index 0000000..09adbb5 --- /dev/null +++ b/tests/results/0206_assign_add.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [7;7] ] diff --git a/tests/results/0206_assign_add.polyhedra.txt b/tests/results/0206_assign_add.polyhedra.txt new file mode 100644 index 0000000..532172f --- /dev/null +++ b/tests/results/0206_assign_add.polyhedra.txt @@ -0,0 +1 @@ +Output: [|x-7=0|] diff --git a/tests/results/0207_assign_add2.constants.txt b/tests/results/0207_assign_add2.constants.txt new file mode 100644 index 0000000..1e125b7 --- /dev/null +++ b/tests/results/0207_assign_add2.constants.txt @@ -0,0 +1 @@ +Output: [ x in top ] diff --git a/tests/results/0207_assign_add2.intervals.txt b/tests/results/0207_assign_add2.intervals.txt new file mode 100644 index 0000000..8b42f78 --- /dev/null +++ b/tests/results/0207_assign_add2.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [11;15] ] diff --git a/tests/results/0207_assign_add2.polyhedra.txt b/tests/results/0207_assign_add2.polyhedra.txt new file mode 100644 index 0000000..9ea10ba --- /dev/null +++ b/tests/results/0207_assign_add2.polyhedra.txt @@ -0,0 +1 @@ +Output: [|-x+15>=0; x-11>=0|] diff --git a/tests/results/0208_assign_add3.constants.txt b/tests/results/0208_assign_add3.constants.txt new file mode 100644 index 0000000..1e125b7 --- /dev/null +++ b/tests/results/0208_assign_add3.constants.txt @@ -0,0 +1 @@ +Output: [ x in top ] diff --git a/tests/results/0208_assign_add3.intervals.txt b/tests/results/0208_assign_add3.intervals.txt new file mode 100644 index 0000000..eda51d2 --- /dev/null +++ b/tests/results/0208_assign_add3.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [-oo;+oo] ] diff --git a/tests/results/0208_assign_add3.polyhedra.txt b/tests/results/0208_assign_add3.polyhedra.txt new file mode 100644 index 0000000..f62b6cf --- /dev/null +++ b/tests/results/0208_assign_add3.polyhedra.txt @@ -0,0 +1 @@ +Output: top diff --git a/tests/results/0209_assign_neg.constants.txt b/tests/results/0209_assign_neg.constants.txt new file mode 100644 index 0000000..0f5f195 --- /dev/null +++ b/tests/results/0209_assign_neg.constants.txt @@ -0,0 +1 @@ +Output: [ x in {-9} ] diff --git a/tests/results/0209_assign_neg.intervals.txt b/tests/results/0209_assign_neg.intervals.txt new file mode 100644 index 0000000..0fd9c55 --- /dev/null +++ b/tests/results/0209_assign_neg.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [-9;-9] ] diff --git a/tests/results/0209_assign_neg.polyhedra.txt b/tests/results/0209_assign_neg.polyhedra.txt new file mode 100644 index 0000000..6781630 --- /dev/null +++ b/tests/results/0209_assign_neg.polyhedra.txt @@ -0,0 +1 @@ +Output: [|x+9=0|] diff --git a/tests/results/0210_assign_neg2.constants.txt b/tests/results/0210_assign_neg2.constants.txt new file mode 100644 index 0000000..1e125b7 --- /dev/null +++ b/tests/results/0210_assign_neg2.constants.txt @@ -0,0 +1 @@ +Output: [ x in top ] diff --git a/tests/results/0210_assign_neg2.intervals.txt b/tests/results/0210_assign_neg2.intervals.txt new file mode 100644 index 0000000..73d88cf --- /dev/null +++ b/tests/results/0210_assign_neg2.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [-10;1] ] diff --git a/tests/results/0210_assign_neg2.polyhedra.txt b/tests/results/0210_assign_neg2.polyhedra.txt new file mode 100644 index 0000000..072f308 --- /dev/null +++ b/tests/results/0210_assign_neg2.polyhedra.txt @@ -0,0 +1 @@ +Output: [|-x+1>=0; x+10>=0|] diff --git a/tests/results/0211_assign_sub.constants.txt b/tests/results/0211_assign_sub.constants.txt new file mode 100644 index 0000000..081af4c --- /dev/null +++ b/tests/results/0211_assign_sub.constants.txt @@ -0,0 +1 @@ +Output: [ x in {998} ] diff --git a/tests/results/0211_assign_sub.intervals.txt b/tests/results/0211_assign_sub.intervals.txt new file mode 100644 index 0000000..399e33f --- /dev/null +++ b/tests/results/0211_assign_sub.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [998;998] ] diff --git a/tests/results/0211_assign_sub.polyhedra.txt b/tests/results/0211_assign_sub.polyhedra.txt new file mode 100644 index 0000000..c769276 --- /dev/null +++ b/tests/results/0211_assign_sub.polyhedra.txt @@ -0,0 +1 @@ +Output: [|x-998=0|] diff --git a/tests/results/0212_assign_sub2.constants.txt b/tests/results/0212_assign_sub2.constants.txt new file mode 100644 index 0000000..1e125b7 --- /dev/null +++ b/tests/results/0212_assign_sub2.constants.txt @@ -0,0 +1 @@ +Output: [ x in top ] diff --git a/tests/results/0212_assign_sub2.intervals.txt b/tests/results/0212_assign_sub2.intervals.txt new file mode 100644 index 0000000..7280868 --- /dev/null +++ b/tests/results/0212_assign_sub2.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [-2;8] ] diff --git a/tests/results/0212_assign_sub2.polyhedra.txt b/tests/results/0212_assign_sub2.polyhedra.txt new file mode 100644 index 0000000..677491d --- /dev/null +++ b/tests/results/0212_assign_sub2.polyhedra.txt @@ -0,0 +1 @@ +Output: [|-x+8>=0; x+2>=0|] diff --git a/tests/results/0213_assign_mul.constants.txt b/tests/results/0213_assign_mul.constants.txt new file mode 100644 index 0000000..a96ffa9 --- /dev/null +++ b/tests/results/0213_assign_mul.constants.txt @@ -0,0 +1 @@ +Output: [ x in {40} ] diff --git a/tests/results/0213_assign_mul.intervals.txt b/tests/results/0213_assign_mul.intervals.txt new file mode 100644 index 0000000..c4b8532 --- /dev/null +++ b/tests/results/0213_assign_mul.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [40;40] ] diff --git a/tests/results/0213_assign_mul.polyhedra.txt b/tests/results/0213_assign_mul.polyhedra.txt new file mode 100644 index 0000000..c6ed2d5 --- /dev/null +++ b/tests/results/0213_assign_mul.polyhedra.txt @@ -0,0 +1 @@ +Output: [|x-40=0|] diff --git a/tests/results/0214_assign_mul2.constants.txt b/tests/results/0214_assign_mul2.constants.txt new file mode 100644 index 0000000..1e125b7 --- /dev/null +++ b/tests/results/0214_assign_mul2.constants.txt @@ -0,0 +1 @@ +Output: [ x in top ] diff --git a/tests/results/0214_assign_mul2.intervals.txt b/tests/results/0214_assign_mul2.intervals.txt new file mode 100644 index 0000000..73894e9 --- /dev/null +++ b/tests/results/0214_assign_mul2.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [2;27] ] diff --git a/tests/results/0214_assign_mul2.polyhedra.txt b/tests/results/0214_assign_mul2.polyhedra.txt new file mode 100644 index 0000000..8994ea9 --- /dev/null +++ b/tests/results/0214_assign_mul2.polyhedra.txt @@ -0,0 +1 @@ +Output: [|-x+27>=0; x-2>=0|] diff --git a/tests/results/0215_assign_mul3.constants.txt b/tests/results/0215_assign_mul3.constants.txt new file mode 100644 index 0000000..1e125b7 --- /dev/null +++ b/tests/results/0215_assign_mul3.constants.txt @@ -0,0 +1 @@ +Output: [ x in top ] diff --git a/tests/results/0215_assign_mul3.intervals.txt b/tests/results/0215_assign_mul3.intervals.txt new file mode 100644 index 0000000..ed9922e --- /dev/null +++ b/tests/results/0215_assign_mul3.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [-50;30] ] diff --git a/tests/results/0215_assign_mul3.polyhedra.txt b/tests/results/0215_assign_mul3.polyhedra.txt new file mode 100644 index 0000000..245e58b --- /dev/null +++ b/tests/results/0215_assign_mul3.polyhedra.txt @@ -0,0 +1 @@ +Output: [|-x+30>=0; x+50>=0|] diff --git a/tests/results/0216_assign_mul4.constants.txt b/tests/results/0216_assign_mul4.constants.txt new file mode 100644 index 0000000..6423d75 --- /dev/null +++ b/tests/results/0216_assign_mul4.constants.txt @@ -0,0 +1 @@ +Output: [ x in {0} ] diff --git a/tests/results/0216_assign_mul4.intervals.txt b/tests/results/0216_assign_mul4.intervals.txt new file mode 100644 index 0000000..9fe0945 --- /dev/null +++ b/tests/results/0216_assign_mul4.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [0;0] ] diff --git a/tests/results/0216_assign_mul4.polyhedra.txt b/tests/results/0216_assign_mul4.polyhedra.txt new file mode 100644 index 0000000..072e333 --- /dev/null +++ b/tests/results/0216_assign_mul4.polyhedra.txt @@ -0,0 +1 @@ +Output: [|x=0|] diff --git a/tests/results/0217_assign_copy.constants.txt b/tests/results/0217_assign_copy.constants.txt new file mode 100644 index 0000000..48ead4c --- /dev/null +++ b/tests/results/0217_assign_copy.constants.txt @@ -0,0 +1,2 @@ +sources/0217_assign_copy.c:5.0-9: [ y in {12} ] +Output: [ x in {12}, y in {12} ] diff --git a/tests/results/0217_assign_copy.intervals.txt b/tests/results/0217_assign_copy.intervals.txt new file mode 100644 index 0000000..deede7b --- /dev/null +++ b/tests/results/0217_assign_copy.intervals.txt @@ -0,0 +1,2 @@ +sources/0217_assign_copy.c:5.0-9: [ y in [12;12] ] +Output: [ x in [12;12], y in [12;12] ] diff --git a/tests/results/0217_assign_copy.polyhedra.txt b/tests/results/0217_assign_copy.polyhedra.txt new file mode 100644 index 0000000..2390288 --- /dev/null +++ b/tests/results/0217_assign_copy.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0217_assign_copy.c:5.0-9: [|y-12=0|] +Output: [|y-12=0; x-12=0|] diff --git a/tests/results/0218_assign_rel.constants.txt b/tests/results/0218_assign_rel.constants.txt new file mode 100644 index 0000000..33b1a1f --- /dev/null +++ b/tests/results/0218_assign_rel.constants.txt @@ -0,0 +1,2 @@ +sources/0218_assign_rel.c:5.0-9: [ y in {17} ] +Output: [ x in {15}, y in {17} ] diff --git a/tests/results/0218_assign_rel.intervals.txt b/tests/results/0218_assign_rel.intervals.txt new file mode 100644 index 0000000..3972546 --- /dev/null +++ b/tests/results/0218_assign_rel.intervals.txt @@ -0,0 +1,2 @@ +sources/0218_assign_rel.c:5.0-9: [ y in [17;17] ] +Output: [ x in [15;15], y in [17;17] ] diff --git a/tests/results/0218_assign_rel.polyhedra.txt b/tests/results/0218_assign_rel.polyhedra.txt new file mode 100644 index 0000000..4a1f8dd --- /dev/null +++ b/tests/results/0218_assign_rel.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0218_assign_rel.c:5.0-9: [|y-17=0|] +Output: [|y-17=0; x-15=0|] diff --git a/tests/results/0219_assign_rel2.constants.txt b/tests/results/0219_assign_rel2.constants.txt new file mode 100644 index 0000000..8204d04 --- /dev/null +++ b/tests/results/0219_assign_rel2.constants.txt @@ -0,0 +1 @@ +Output: [ x in top, y in top, z in top ] diff --git a/tests/results/0219_assign_rel2.intervals.txt b/tests/results/0219_assign_rel2.intervals.txt new file mode 100644 index 0000000..6225596 --- /dev/null +++ b/tests/results/0219_assign_rel2.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [1;5], y in [2;10], z in [5;25] ] diff --git a/tests/results/0219_assign_rel2.polyhedra.txt b/tests/results/0219_assign_rel2.polyhedra.txt new file mode 100644 index 0000000..08949e1 --- /dev/null +++ b/tests/results/0219_assign_rel2.polyhedra.txt @@ -0,0 +1 @@ +Output: [|-x-2y+z=0; -x+5>=0; -y+10>=0; y-2>=0; x-1>=0|] diff --git a/tests/results/0300_if_true.constants.txt b/tests/results/0300_if_true.constants.txt new file mode 100644 index 0000000..d462831 --- /dev/null +++ b/tests/results/0300_if_true.constants.txt @@ -0,0 +1 @@ +Output: [ x in {9} ] diff --git a/tests/results/0300_if_true.intervals.txt b/tests/results/0300_if_true.intervals.txt new file mode 100644 index 0000000..0c6f646 --- /dev/null +++ b/tests/results/0300_if_true.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [9;9] ] diff --git a/tests/results/0300_if_true.polyhedra.txt b/tests/results/0300_if_true.polyhedra.txt new file mode 100644 index 0000000..90a38c5 --- /dev/null +++ b/tests/results/0300_if_true.polyhedra.txt @@ -0,0 +1 @@ +Output: [|x-9=0|] diff --git a/tests/results/0301_if_false.constants.txt b/tests/results/0301_if_false.constants.txt new file mode 100644 index 0000000..ebf94f0 --- /dev/null +++ b/tests/results/0301_if_false.constants.txt @@ -0,0 +1 @@ +Output: [ x in {1} ] diff --git a/tests/results/0301_if_false.intervals.txt b/tests/results/0301_if_false.intervals.txt new file mode 100644 index 0000000..725d6cd --- /dev/null +++ b/tests/results/0301_if_false.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [1;1] ] diff --git a/tests/results/0301_if_false.polyhedra.txt b/tests/results/0301_if_false.polyhedra.txt new file mode 100644 index 0000000..ea9534b --- /dev/null +++ b/tests/results/0301_if_false.polyhedra.txt @@ -0,0 +1 @@ +Output: [|x-1=0|] diff --git a/tests/results/0302_if_both.constants.txt b/tests/results/0302_if_both.constants.txt new file mode 100644 index 0000000..1e125b7 --- /dev/null +++ b/tests/results/0302_if_both.constants.txt @@ -0,0 +1 @@ +Output: [ x in top ] diff --git a/tests/results/0302_if_both.intervals.txt b/tests/results/0302_if_both.intervals.txt new file mode 100644 index 0000000..325829f --- /dev/null +++ b/tests/results/0302_if_both.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [1;9] ] diff --git a/tests/results/0302_if_both.polyhedra.txt b/tests/results/0302_if_both.polyhedra.txt new file mode 100644 index 0000000..f9f53a2 --- /dev/null +++ b/tests/results/0302_if_both.polyhedra.txt @@ -0,0 +1 @@ +Output: [|-x+9>=0; x-1>=0|] diff --git a/tests/results/0303_if_else_true.constants.txt b/tests/results/0303_if_else_true.constants.txt new file mode 100644 index 0000000..a5cfc34 --- /dev/null +++ b/tests/results/0303_if_else_true.constants.txt @@ -0,0 +1 @@ +Output: [ x in {5} ] diff --git a/tests/results/0303_if_else_true.intervals.txt b/tests/results/0303_if_else_true.intervals.txt new file mode 100644 index 0000000..215f0dd --- /dev/null +++ b/tests/results/0303_if_else_true.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [5;5] ] diff --git a/tests/results/0303_if_else_true.polyhedra.txt b/tests/results/0303_if_else_true.polyhedra.txt new file mode 100644 index 0000000..257804b --- /dev/null +++ b/tests/results/0303_if_else_true.polyhedra.txt @@ -0,0 +1 @@ +Output: [|x-5=0|] diff --git a/tests/results/0304_if_else_false.constants.txt b/tests/results/0304_if_else_false.constants.txt new file mode 100644 index 0000000..8bda3f6 --- /dev/null +++ b/tests/results/0304_if_else_false.constants.txt @@ -0,0 +1 @@ +Output: [ x in {10} ] diff --git a/tests/results/0304_if_else_false.intervals.txt b/tests/results/0304_if_else_false.intervals.txt new file mode 100644 index 0000000..fc10743 --- /dev/null +++ b/tests/results/0304_if_else_false.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [10;10] ] diff --git a/tests/results/0304_if_else_false.polyhedra.txt b/tests/results/0304_if_else_false.polyhedra.txt new file mode 100644 index 0000000..4824605 --- /dev/null +++ b/tests/results/0304_if_else_false.polyhedra.txt @@ -0,0 +1 @@ +Output: [|x-10=0|] diff --git a/tests/results/0305_if_else_both.constants.txt b/tests/results/0305_if_else_both.constants.txt new file mode 100644 index 0000000..1e125b7 --- /dev/null +++ b/tests/results/0305_if_else_both.constants.txt @@ -0,0 +1 @@ +Output: [ x in top ] diff --git a/tests/results/0305_if_else_both.intervals.txt b/tests/results/0305_if_else_both.intervals.txt new file mode 100644 index 0000000..5094331 --- /dev/null +++ b/tests/results/0305_if_else_both.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [5;10] ] diff --git a/tests/results/0305_if_else_both.polyhedra.txt b/tests/results/0305_if_else_both.polyhedra.txt new file mode 100644 index 0000000..5cee0c4 --- /dev/null +++ b/tests/results/0305_if_else_both.polyhedra.txt @@ -0,0 +1 @@ +Output: [|-x+10>=0; x-5>=0|] diff --git a/tests/results/0306_if_rel.constants.txt b/tests/results/0306_if_rel.constants.txt new file mode 100644 index 0000000..b7ada66 --- /dev/null +++ b/tests/results/0306_if_rel.constants.txt @@ -0,0 +1 @@ +Output: [ x in top, y in top ] diff --git a/tests/results/0306_if_rel.intervals.txt b/tests/results/0306_if_rel.intervals.txt new file mode 100644 index 0000000..720b91a --- /dev/null +++ b/tests/results/0306_if_rel.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [1;2], y in [1;3] ] diff --git a/tests/results/0306_if_rel.polyhedra.txt b/tests/results/0306_if_rel.polyhedra.txt new file mode 100644 index 0000000..d98e52e --- /dev/null +++ b/tests/results/0306_if_rel.polyhedra.txt @@ -0,0 +1 @@ +Output: [|2x+y-5=0; -x+2>=0; x-1>=0|] diff --git a/tests/results/0307_if_var.constants.txt b/tests/results/0307_if_var.constants.txt new file mode 100644 index 0000000..d30fa5d --- /dev/null +++ b/tests/results/0307_if_var.constants.txt @@ -0,0 +1,3 @@ +sources/0307_if_var.c:2.14-24: [ x in top ] +sources/0307_if_var.c:3.7-17: [ x in top ] +Output: [ x in top ] diff --git a/tests/results/0307_if_var.intervals.txt b/tests/results/0307_if_var.intervals.txt new file mode 100644 index 0000000..2290fb8 --- /dev/null +++ b/tests/results/0307_if_var.intervals.txt @@ -0,0 +1,3 @@ +sources/0307_if_var.c:2.14-24: [ x in [0;20] ] +sources/0307_if_var.c:3.7-17: [ x in [-10;-1] ] +Output: [ x in [-10;20] ] diff --git a/tests/results/0307_if_var.polyhedra.txt b/tests/results/0307_if_var.polyhedra.txt new file mode 100644 index 0000000..c9e0e7a --- /dev/null +++ b/tests/results/0307_if_var.polyhedra.txt @@ -0,0 +1,3 @@ +sources/0307_if_var.c:2.14-24: [|-x+20>=0; x>=0|] +sources/0307_if_var.c:3.7-17: [|-x-1>=0; x+10>=0|] +Output: [|-x+20>=0; x+10>=0|] diff --git a/tests/results/0308_if_var2.constants.txt b/tests/results/0308_if_var2.constants.txt new file mode 100644 index 0000000..1e125b7 --- /dev/null +++ b/tests/results/0308_if_var2.constants.txt @@ -0,0 +1 @@ +Output: [ x in top ] diff --git a/tests/results/0308_if_var2.intervals.txt b/tests/results/0308_if_var2.intervals.txt new file mode 100644 index 0000000..534d2d3 --- /dev/null +++ b/tests/results/0308_if_var2.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [-1;20] ] diff --git a/tests/results/0308_if_var2.polyhedra.txt b/tests/results/0308_if_var2.polyhedra.txt new file mode 100644 index 0000000..3378d1d --- /dev/null +++ b/tests/results/0308_if_var2.polyhedra.txt @@ -0,0 +1 @@ +Output: [|-x+20>=0; x+1>=0|] diff --git a/tests/results/0309_if_var_rel.constants.txt b/tests/results/0309_if_var_rel.constants.txt new file mode 100644 index 0000000..b7ada66 --- /dev/null +++ b/tests/results/0309_if_var_rel.constants.txt @@ -0,0 +1 @@ +Output: [ x in top, y in top ] diff --git a/tests/results/0309_if_var_rel.intervals.txt b/tests/results/0309_if_var_rel.intervals.txt new file mode 100644 index 0000000..a61ddd6 --- /dev/null +++ b/tests/results/0309_if_var_rel.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [-15;20], y in [-15;20] ] diff --git a/tests/results/0309_if_var_rel.polyhedra.txt b/tests/results/0309_if_var_rel.polyhedra.txt new file mode 100644 index 0000000..c11732e --- /dev/null +++ b/tests/results/0309_if_var_rel.polyhedra.txt @@ -0,0 +1 @@ +Output: [|-x+y>=0; -y+20>=0; 7x-y+90>=0|] diff --git a/tests/results/0310_cmp_le.constants.txt b/tests/results/0310_cmp_le.constants.txt new file mode 100644 index 0000000..b88d9db --- /dev/null +++ b/tests/results/0310_cmp_le.constants.txt @@ -0,0 +1,2 @@ +sources/0310_cmp_le.c:3.11-23: [ x in top, y in top ] +Output: [ x in top, y in top ] diff --git a/tests/results/0310_cmp_le.intervals.txt b/tests/results/0310_cmp_le.intervals.txt new file mode 100644 index 0000000..186a3c3 --- /dev/null +++ b/tests/results/0310_cmp_le.intervals.txt @@ -0,0 +1,2 @@ +sources/0310_cmp_le.c:3.11-23: [ x in [10;20], y in [15;30] ] +Output: [ x in [10;20], y in [15;30] ] diff --git a/tests/results/0310_cmp_le.polyhedra.txt b/tests/results/0310_cmp_le.polyhedra.txt new file mode 100644 index 0000000..d7bcb41 --- /dev/null +++ b/tests/results/0310_cmp_le.polyhedra.txt @@ -0,0 +1,3 @@ +sources/0310_cmp_le.c:3.11-23: [|-x+20>=0; -x+y>=0; -y+30>=0; y-15>=0; + x-10>=0|] +Output: [|-x+20>=0; -y+30>=0; y-15>=0; x-10>=0|] diff --git a/tests/results/0311_cmp_le2.constants.txt b/tests/results/0311_cmp_le2.constants.txt new file mode 100644 index 0000000..6a9db98 --- /dev/null +++ b/tests/results/0311_cmp_le2.constants.txt @@ -0,0 +1,2 @@ +sources/0311_cmp_le2.c:3.11-23: [ x in top, y in top ] +Output: [ x in top, y in top ] diff --git a/tests/results/0311_cmp_le2.intervals.txt b/tests/results/0311_cmp_le2.intervals.txt new file mode 100644 index 0000000..1c2ca5a --- /dev/null +++ b/tests/results/0311_cmp_le2.intervals.txt @@ -0,0 +1,2 @@ +sources/0311_cmp_le2.c:3.11-23: [ x in [10;17], y in [10;17] ] +Output: [ x in [10;20], y in [8;17] ] diff --git a/tests/results/0311_cmp_le2.polyhedra.txt b/tests/results/0311_cmp_le2.polyhedra.txt new file mode 100644 index 0000000..6fc97d1 --- /dev/null +++ b/tests/results/0311_cmp_le2.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0311_cmp_le2.c:3.11-23: [|-x+y>=0; -y+17>=0; x-10>=0|] +Output: [|-x+20>=0; -y+17>=0; y-8>=0; x-10>=0|] diff --git a/tests/results/0312_cmp_le3.constants.txt b/tests/results/0312_cmp_le3.constants.txt new file mode 100644 index 0000000..748bd4b --- /dev/null +++ b/tests/results/0312_cmp_le3.constants.txt @@ -0,0 +1,2 @@ +sources/0312_cmp_le3.c:3.11-21: [ x in top ] +Output: [ x in top, y in top ] diff --git a/tests/results/0312_cmp_le3.intervals.txt b/tests/results/0312_cmp_le3.intervals.txt new file mode 100644 index 0000000..908661c --- /dev/null +++ b/tests/results/0312_cmp_le3.intervals.txt @@ -0,0 +1,2 @@ +sources/0312_cmp_le3.c:3.11-21: bottom +Output: [ x in [30;55], y in [10;20] ] diff --git a/tests/results/0312_cmp_le3.polyhedra.txt b/tests/results/0312_cmp_le3.polyhedra.txt new file mode 100644 index 0000000..32ffc17 --- /dev/null +++ b/tests/results/0312_cmp_le3.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0312_cmp_le3.c:3.11-21: bottom +Output: [|-x+55>=0; -y+20>=0; y-10>=0; x-30>=0|] diff --git a/tests/results/0313_cmp_lt.constants.txt b/tests/results/0313_cmp_lt.constants.txt new file mode 100644 index 0000000..3685d47 --- /dev/null +++ b/tests/results/0313_cmp_lt.constants.txt @@ -0,0 +1,2 @@ +sources/0313_cmp_lt.c:3.10-22: [ x in top, y in top ] +Output: [ x in top, y in top ] diff --git a/tests/results/0313_cmp_lt.intervals.txt b/tests/results/0313_cmp_lt.intervals.txt new file mode 100644 index 0000000..3826912 --- /dev/null +++ b/tests/results/0313_cmp_lt.intervals.txt @@ -0,0 +1,2 @@ +sources/0313_cmp_lt.c:3.10-22: [ x in [10;14], y in [11;15] ] +Output: [ x in [10;20], y in [5;15] ] diff --git a/tests/results/0313_cmp_lt.polyhedra.txt b/tests/results/0313_cmp_lt.polyhedra.txt new file mode 100644 index 0000000..d70d1cc --- /dev/null +++ b/tests/results/0313_cmp_lt.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0313_cmp_lt.c:3.10-22: [|-x+y-1>=0; -y+15>=0; x-10>=0|] +Output: [|-x+20>=0; -y+15>=0; y-5>=0; x-10>=0|] diff --git a/tests/results/0314_cmp_ge.constants.txt b/tests/results/0314_cmp_ge.constants.txt new file mode 100644 index 0000000..7722930 --- /dev/null +++ b/tests/results/0314_cmp_ge.constants.txt @@ -0,0 +1,2 @@ +sources/0314_cmp_ge.c:3.11-23: [ x in top, y in top ] +Output: [ x in top, y in top ] diff --git a/tests/results/0314_cmp_ge.intervals.txt b/tests/results/0314_cmp_ge.intervals.txt new file mode 100644 index 0000000..e49273e --- /dev/null +++ b/tests/results/0314_cmp_ge.intervals.txt @@ -0,0 +1,2 @@ +sources/0314_cmp_ge.c:3.11-23: [ x in [15;20], y in [15;20] ] +Output: [ x in [10;20], y in [15;30] ] diff --git a/tests/results/0314_cmp_ge.polyhedra.txt b/tests/results/0314_cmp_ge.polyhedra.txt new file mode 100644 index 0000000..74534e2 --- /dev/null +++ b/tests/results/0314_cmp_ge.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0314_cmp_ge.c:3.11-23: [|-x+20>=0; y-15>=0; x-y>=0|] +Output: [|-x+20>=0; -y+30>=0; y-15>=0; x-10>=0|] diff --git a/tests/results/0315_cmp_gt.constants.txt b/tests/results/0315_cmp_gt.constants.txt new file mode 100644 index 0000000..8c9b15f --- /dev/null +++ b/tests/results/0315_cmp_gt.constants.txt @@ -0,0 +1,2 @@ +sources/0315_cmp_gt.c:3.10-22: [ x in top, y in top ] +Output: [ x in top, y in top ] diff --git a/tests/results/0315_cmp_gt.intervals.txt b/tests/results/0315_cmp_gt.intervals.txt new file mode 100644 index 0000000..f8b07c0 --- /dev/null +++ b/tests/results/0315_cmp_gt.intervals.txt @@ -0,0 +1,2 @@ +sources/0315_cmp_gt.c:3.10-22: [ x in [16;20], y in [15;19] ] +Output: [ x in [10;20], y in [15;30] ] diff --git a/tests/results/0315_cmp_gt.polyhedra.txt b/tests/results/0315_cmp_gt.polyhedra.txt new file mode 100644 index 0000000..2418ec8 --- /dev/null +++ b/tests/results/0315_cmp_gt.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0315_cmp_gt.c:3.10-22: [|-x+20>=0; y-15>=0; x-y-1>=0|] +Output: [|-x+20>=0; -y+30>=0; y-15>=0; x-10>=0|] diff --git a/tests/results/0316_cmp_eq.constants.txt b/tests/results/0316_cmp_eq.constants.txt new file mode 100644 index 0000000..2cf2cae --- /dev/null +++ b/tests/results/0316_cmp_eq.constants.txt @@ -0,0 +1,2 @@ +sources/0316_cmp_eq.c:3.11-23: [ x in top, y in top ] +Output: [ x in top, y in top ] diff --git a/tests/results/0316_cmp_eq.intervals.txt b/tests/results/0316_cmp_eq.intervals.txt new file mode 100644 index 0000000..46c87c8 --- /dev/null +++ b/tests/results/0316_cmp_eq.intervals.txt @@ -0,0 +1,2 @@ +sources/0316_cmp_eq.c:3.11-23: [ x in [15;20], y in [15;20] ] +Output: [ x in [15;30], y in [10;20] ] diff --git a/tests/results/0316_cmp_eq.polyhedra.txt b/tests/results/0316_cmp_eq.polyhedra.txt new file mode 100644 index 0000000..abf553c --- /dev/null +++ b/tests/results/0316_cmp_eq.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0316_cmp_eq.c:3.11-23: [|-x+y=0; -x+20>=0; x-15>=0|] +Output: [|-x+30>=0; -y+20>=0; y-10>=0; x-15>=0|] diff --git a/tests/results/0317_cmp_eq2.constants.txt b/tests/results/0317_cmp_eq2.constants.txt new file mode 100644 index 0000000..81a43de --- /dev/null +++ b/tests/results/0317_cmp_eq2.constants.txt @@ -0,0 +1,2 @@ +sources/0317_cmp_eq2.c:3.11-23: [ x in top, y in top ] +Output: [ x in top, y in top ] diff --git a/tests/results/0317_cmp_eq2.intervals.txt b/tests/results/0317_cmp_eq2.intervals.txt new file mode 100644 index 0000000..93841ec --- /dev/null +++ b/tests/results/0317_cmp_eq2.intervals.txt @@ -0,0 +1,2 @@ +sources/0317_cmp_eq2.c:3.11-23: bottom +Output: [ x in [15;20], y in [25;30] ] diff --git a/tests/results/0317_cmp_eq2.polyhedra.txt b/tests/results/0317_cmp_eq2.polyhedra.txt new file mode 100644 index 0000000..c6ba540 --- /dev/null +++ b/tests/results/0317_cmp_eq2.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0317_cmp_eq2.c:3.11-23: bottom +Output: [|-x+20>=0; -y+30>=0; y-25>=0; x-15>=0|] diff --git a/tests/results/0318_cmp_ne.constants.txt b/tests/results/0318_cmp_ne.constants.txt new file mode 100644 index 0000000..f95b2e8 --- /dev/null +++ b/tests/results/0318_cmp_ne.constants.txt @@ -0,0 +1,2 @@ +sources/0318_cmp_ne.c:3.11-23: [ x in top, y in top ] +Output: [ x in top, y in top ] diff --git a/tests/results/0318_cmp_ne.intervals.txt b/tests/results/0318_cmp_ne.intervals.txt new file mode 100644 index 0000000..5908089 --- /dev/null +++ b/tests/results/0318_cmp_ne.intervals.txt @@ -0,0 +1,2 @@ +sources/0318_cmp_ne.c:3.11-23: [ x in [10;15], y in [10;15] ] +Output: [ x in [10;15], y in [10;15] ] diff --git a/tests/results/0318_cmp_ne.polyhedra.txt b/tests/results/0318_cmp_ne.polyhedra.txt new file mode 100644 index 0000000..8008082 --- /dev/null +++ b/tests/results/0318_cmp_ne.polyhedra.txt @@ -0,0 +1,3 @@ +sources/0318_cmp_ne.c:3.11-23: [|-x-y+29>=0; -x+15>=0; -y+15>=0; y-10>=0; + x-10>=0; x+y-21>=0|] +Output: [|-x+15>=0; -y+15>=0; y-10>=0; x-10>=0|] diff --git a/tests/results/0319_cmp_ne.constants.txt b/tests/results/0319_cmp_ne.constants.txt new file mode 100644 index 0000000..80005f9 --- /dev/null +++ b/tests/results/0319_cmp_ne.constants.txt @@ -0,0 +1,2 @@ +sources/0319_cmp_ne.c:3.11-23: [ x in top, y in {10} ] +Output: [ x in top, y in {10} ] diff --git a/tests/results/0319_cmp_ne.intervals.txt b/tests/results/0319_cmp_ne.intervals.txt new file mode 100644 index 0000000..cfd42ac --- /dev/null +++ b/tests/results/0319_cmp_ne.intervals.txt @@ -0,0 +1,2 @@ +sources/0319_cmp_ne.c:3.11-23: [ x in [11;15], y in [10;10] ] +Output: [ x in [10;15], y in [10;10] ] diff --git a/tests/results/0319_cmp_ne.polyhedra.txt b/tests/results/0319_cmp_ne.polyhedra.txt new file mode 100644 index 0000000..68272de --- /dev/null +++ b/tests/results/0319_cmp_ne.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0319_cmp_ne.c:3.11-23: [|y-10=0; -x+15>=0; x-11>=0|] +Output: [|y-10=0; -x+15>=0; x-10>=0|] diff --git a/tests/results/0320_cmp_eq_ne.constants.txt b/tests/results/0320_cmp_eq_ne.constants.txt new file mode 100644 index 0000000..d09e55d --- /dev/null +++ b/tests/results/0320_cmp_eq_ne.constants.txt @@ -0,0 +1,3 @@ +sources/0320_cmp_eq_ne.c:3.11-4.0: [ x in {10}, y in {10} ] +sources/0320_cmp_eq_ne.c:4.4-16: [ x in top, y in {10} ] +Output: [ x in top, y in {10} ] diff --git a/tests/results/0320_cmp_eq_ne.intervals.txt b/tests/results/0320_cmp_eq_ne.intervals.txt new file mode 100644 index 0000000..696f4f7 --- /dev/null +++ b/tests/results/0320_cmp_eq_ne.intervals.txt @@ -0,0 +1,3 @@ +sources/0320_cmp_eq_ne.c:3.11-4.0: [ x in [10;10], y in [10;10] ] +sources/0320_cmp_eq_ne.c:4.4-16: [ x in [11;15], y in [10;10] ] +Output: [ x in [10;15], y in [10;10] ] diff --git a/tests/results/0320_cmp_eq_ne.polyhedra.txt b/tests/results/0320_cmp_eq_ne.polyhedra.txt new file mode 100644 index 0000000..82585b7 --- /dev/null +++ b/tests/results/0320_cmp_eq_ne.polyhedra.txt @@ -0,0 +1,3 @@ +sources/0320_cmp_eq_ne.c:3.11-4.0: [|y-10=0; x-10=0|] +sources/0320_cmp_eq_ne.c:4.4-16: [|y-10=0; -x+15>=0; x-11>=0|] +Output: [|y-10=0; -x+15>=0; x-10>=0|] diff --git a/tests/results/0321_cmp_rel.constants.txt b/tests/results/0321_cmp_rel.constants.txt new file mode 100644 index 0000000..8cbd76e --- /dev/null +++ b/tests/results/0321_cmp_rel.constants.txt @@ -0,0 +1,2 @@ +sources/0321_cmp_rel.c:3.15-25: [ y in top ] +Output: [ x in top, y in top ] diff --git a/tests/results/0321_cmp_rel.intervals.txt b/tests/results/0321_cmp_rel.intervals.txt new file mode 100644 index 0000000..0916a62 --- /dev/null +++ b/tests/results/0321_cmp_rel.intervals.txt @@ -0,0 +1,2 @@ +sources/0321_cmp_rel.c:3.15-25: [ y in [10;20] ] +Output: [ x in [10;20], y in [10;20] ] diff --git a/tests/results/0321_cmp_rel.polyhedra.txt b/tests/results/0321_cmp_rel.polyhedra.txt new file mode 100644 index 0000000..7a04a8a --- /dev/null +++ b/tests/results/0321_cmp_rel.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0321_cmp_rel.c:3.15-25: [|-y+20>=0; y-15>=0|] +Output: [|-x+y=0; -x+20>=0; x-10>=0|] diff --git a/tests/results/0322_if_and.constants.txt b/tests/results/0322_if_and.constants.txt new file mode 100644 index 0000000..220ba86 --- /dev/null +++ b/tests/results/0322_if_and.constants.txt @@ -0,0 +1,3 @@ +sources/0322_if_and.c:3.22-34: [ x in top, y in top ] +sources/0322_if_and.c:4.7-19: [ x in top, y in top ] +Output: [ x in top, y in top ] diff --git a/tests/results/0322_if_and.intervals.txt b/tests/results/0322_if_and.intervals.txt new file mode 100644 index 0000000..3decd30 --- /dev/null +++ b/tests/results/0322_if_and.intervals.txt @@ -0,0 +1,3 @@ +sources/0322_if_and.c:3.22-34: [ x in [15;20], y in [35;40] ] +sources/0322_if_and.c:4.7-19: [ x in [10;20], y in [30;40] ] +Output: [ x in [10;20], y in [30;40] ] diff --git a/tests/results/0322_if_and.polyhedra.txt b/tests/results/0322_if_and.polyhedra.txt new file mode 100644 index 0000000..691b7ac --- /dev/null +++ b/tests/results/0322_if_and.polyhedra.txt @@ -0,0 +1,4 @@ +sources/0322_if_and.c:3.22-34: [|-x+20>=0; -y+40>=0; y-35>=0; x-15>=0|] +sources/0322_if_and.c:4.7-19: [|-x-y+54>=0; -x+20>=0; -y+40>=0; y-30>=0; + x-10>=0|] +Output: [|-x+20>=0; -y+40>=0; y-30>=0; x-10>=0|] diff --git a/tests/results/0323_if_or.constants.txt b/tests/results/0323_if_or.constants.txt new file mode 100644 index 0000000..8682e63 --- /dev/null +++ b/tests/results/0323_if_or.constants.txt @@ -0,0 +1,3 @@ +sources/0323_if_or.c:3.22-34: [ x in top, y in top ] +sources/0323_if_or.c:4.7-19: [ x in top, y in top ] +Output: [ x in top, y in top ] diff --git a/tests/results/0323_if_or.intervals.txt b/tests/results/0323_if_or.intervals.txt new file mode 100644 index 0000000..039c089 --- /dev/null +++ b/tests/results/0323_if_or.intervals.txt @@ -0,0 +1,3 @@ +sources/0323_if_or.c:3.22-34: [ x in [10;20], y in [30;40] ] +sources/0323_if_or.c:4.7-19: [ x in [10;14], y in [30;34] ] +Output: [ x in [10;20], y in [30;40] ] diff --git a/tests/results/0323_if_or.polyhedra.txt b/tests/results/0323_if_or.polyhedra.txt new file mode 100644 index 0000000..0854d10 --- /dev/null +++ b/tests/results/0323_if_or.polyhedra.txt @@ -0,0 +1,4 @@ +sources/0323_if_or.c:3.22-34: [|-x+20>=0; -y+40>=0; y-30>=0; x-10>=0; + x+y-45>=0|] +sources/0323_if_or.c:4.7-19: [|-x+14>=0; -y+34>=0; y-30>=0; x-10>=0|] +Output: [|-x+20>=0; -y+40>=0; y-30>=0; x-10>=0|] diff --git a/tests/results/0324_if_not.constants.txt b/tests/results/0324_if_not.constants.txt new file mode 100644 index 0000000..9e4038c --- /dev/null +++ b/tests/results/0324_if_not.constants.txt @@ -0,0 +1,3 @@ +sources/0324_if_not.c:3.25-37: [ x in top, y in top ] +sources/0324_if_not.c:4.7-19: [ x in top, y in top ] +Output: [ x in top, y in top ] diff --git a/tests/results/0324_if_not.intervals.txt b/tests/results/0324_if_not.intervals.txt new file mode 100644 index 0000000..e51107a --- /dev/null +++ b/tests/results/0324_if_not.intervals.txt @@ -0,0 +1,3 @@ +sources/0324_if_not.c:3.25-37: [ x in [10;20], y in [30;40] ] +sources/0324_if_not.c:4.7-19: [ x in [15;20], y in [30;34] ] +Output: [ x in [10;20], y in [30;40] ] diff --git a/tests/results/0324_if_not.polyhedra.txt b/tests/results/0324_if_not.polyhedra.txt new file mode 100644 index 0000000..4361881 --- /dev/null +++ b/tests/results/0324_if_not.polyhedra.txt @@ -0,0 +1,4 @@ +sources/0324_if_not.c:3.25-37: [|-5x+6y-110>=0; -x+20>=0; -y+40>=0; y-30>=0; + x-10>=0|] +sources/0324_if_not.c:4.7-19: [|-x+20>=0; -y+34>=0; y-30>=0; x-15>=0|] +Output: [|-x+20>=0; -y+40>=0; y-30>=0; x-10>=0|] diff --git a/tests/results/0325_if_bool.constants.txt b/tests/results/0325_if_bool.constants.txt new file mode 100644 index 0000000..714b57b --- /dev/null +++ b/tests/results/0325_if_bool.constants.txt @@ -0,0 +1,3 @@ +sources/0325_if_bool.c:3.40-52: [ x in top, y in top ] +sources/0325_if_bool.c:4.7-19: [ x in top, y in top ] +Output: [ x in top, y in top ] diff --git a/tests/results/0325_if_bool.intervals.txt b/tests/results/0325_if_bool.intervals.txt new file mode 100644 index 0000000..cd51d25 --- /dev/null +++ b/tests/results/0325_if_bool.intervals.txt @@ -0,0 +1,3 @@ +sources/0325_if_bool.c:3.40-52: [ x in [10;20], y in [10;20] ] +sources/0325_if_bool.c:4.7-19: [ x in [10;20], y in [10;20] ] +Output: [ x in [10;20], y in [10;20] ] diff --git a/tests/results/0325_if_bool.polyhedra.txt b/tests/results/0325_if_bool.polyhedra.txt new file mode 100644 index 0000000..54b93f7 --- /dev/null +++ b/tests/results/0325_if_bool.polyhedra.txt @@ -0,0 +1,5 @@ +sources/0325_if_bool.c:3.40-52: [|-x-y+35>=0; -x+20>=0; -y+20>=0; y-10>=0; + x-10>=0; x+y-25>=0|] +sources/0325_if_bool.c:4.7-19: [|-x+20>=0; -x+y+4>=0; -y+20>=0; y-10>=0; + x-y+4>=0; x-10>=0|] +Output: [|-x+20>=0; -y+20>=0; y-10>=0; x-10>=0|] diff --git a/tests/results/0400_assert_true.constants.txt b/tests/results/0400_assert_true.constants.txt new file mode 100644 index 0000000..7465c26 --- /dev/null +++ b/tests/results/0400_assert_true.constants.txt @@ -0,0 +1 @@ +Output: [ x in {2} ] diff --git a/tests/results/0400_assert_true.intervals.txt b/tests/results/0400_assert_true.intervals.txt new file mode 100644 index 0000000..8aa541a --- /dev/null +++ b/tests/results/0400_assert_true.intervals.txt @@ -0,0 +1 @@ +Output: [ x in [2;2] ] diff --git a/tests/results/0400_assert_true.polyhedra.txt b/tests/results/0400_assert_true.polyhedra.txt new file mode 100644 index 0000000..0472ac6 --- /dev/null +++ b/tests/results/0400_assert_true.polyhedra.txt @@ -0,0 +1 @@ +Output: [|x-2=0|] diff --git a/tests/results/0401_assert_false.constants.txt b/tests/results/0401_assert_false.constants.txt new file mode 100644 index 0000000..2dd50d8 --- /dev/null +++ b/tests/results/0401_assert_false.constants.txt @@ -0,0 +1,2 @@ +sources/0401_assert_false.c:2.0-15: ERROR: assertion failure +Output: bottom diff --git a/tests/results/0401_assert_false.intervals.txt b/tests/results/0401_assert_false.intervals.txt new file mode 100644 index 0000000..2dd50d8 --- /dev/null +++ b/tests/results/0401_assert_false.intervals.txt @@ -0,0 +1,2 @@ +sources/0401_assert_false.c:2.0-15: ERROR: assertion failure +Output: bottom diff --git a/tests/results/0401_assert_false.polyhedra.txt b/tests/results/0401_assert_false.polyhedra.txt new file mode 100644 index 0000000..2dd50d8 --- /dev/null +++ b/tests/results/0401_assert_false.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0401_assert_false.c:2.0-15: ERROR: assertion failure +Output: bottom diff --git a/tests/results/0402_assert_both.constants.txt b/tests/results/0402_assert_both.constants.txt new file mode 100644 index 0000000..f0e4f75 --- /dev/null +++ b/tests/results/0402_assert_both.constants.txt @@ -0,0 +1,3 @@ +sources/0402_assert_both.c:2.0-15: ERROR: assertion failure +sources/0402_assert_both.c:3.0-14: ERROR: assertion failure +Output: [ x in top ] diff --git a/tests/results/0402_assert_both.intervals.txt b/tests/results/0402_assert_both.intervals.txt new file mode 100644 index 0000000..55a8f12 --- /dev/null +++ b/tests/results/0402_assert_both.intervals.txt @@ -0,0 +1,3 @@ +sources/0402_assert_both.c:2.0-15: ERROR: assertion failure +sources/0402_assert_both.c:3.0-14: ERROR: assertion failure +Output: [ x in [1;10] ] diff --git a/tests/results/0402_assert_both.polyhedra.txt b/tests/results/0402_assert_both.polyhedra.txt new file mode 100644 index 0000000..d46828e --- /dev/null +++ b/tests/results/0402_assert_both.polyhedra.txt @@ -0,0 +1,3 @@ +sources/0402_assert_both.c:2.0-15: ERROR: assertion failure +sources/0402_assert_both.c:3.0-14: ERROR: assertion failure +Output: [|-x+10>=0; x-1>=0|] diff --git a/tests/results/0403_assert_both2.constants.txt b/tests/results/0403_assert_both2.constants.txt new file mode 100644 index 0000000..a229c5a --- /dev/null +++ b/tests/results/0403_assert_both2.constants.txt @@ -0,0 +1,3 @@ +sources/0403_assert_both2.c:2.0-14: ERROR: assertion failure +sources/0403_assert_both2.c:3.0-15: ERROR: assertion failure +Output: [ x in top ] diff --git a/tests/results/0403_assert_both2.intervals.txt b/tests/results/0403_assert_both2.intervals.txt new file mode 100644 index 0000000..9dc7efd --- /dev/null +++ b/tests/results/0403_assert_both2.intervals.txt @@ -0,0 +1,2 @@ +sources/0403_assert_both2.c:2.0-14: ERROR: assertion failure +Output: [ x in [1;10] ] diff --git a/tests/results/0403_assert_both2.polyhedra.txt b/tests/results/0403_assert_both2.polyhedra.txt new file mode 100644 index 0000000..37cb40e --- /dev/null +++ b/tests/results/0403_assert_both2.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0403_assert_both2.c:2.0-14: ERROR: assertion failure +Output: [|-x+10>=0; x-1>=0|] diff --git a/tests/results/0404_assert_rel.constants.txt b/tests/results/0404_assert_rel.constants.txt new file mode 100644 index 0000000..2160c42 --- /dev/null +++ b/tests/results/0404_assert_rel.constants.txt @@ -0,0 +1,2 @@ +sources/0404_assert_rel.c:4.0-13: ERROR: assertion failure +Output: [ x in top, y in top ] diff --git a/tests/results/0404_assert_rel.intervals.txt b/tests/results/0404_assert_rel.intervals.txt new file mode 100644 index 0000000..cfcc3b2 --- /dev/null +++ b/tests/results/0404_assert_rel.intervals.txt @@ -0,0 +1,2 @@ +sources/0404_assert_rel.c:4.0-13: ERROR: assertion failure +Output: [ x in [1;3], y in [1;3] ] diff --git a/tests/results/0404_assert_rel.polyhedra.txt b/tests/results/0404_assert_rel.polyhedra.txt new file mode 100644 index 0000000..7b5a252 --- /dev/null +++ b/tests/results/0404_assert_rel.polyhedra.txt @@ -0,0 +1 @@ +Output: [|-x+y=0; -x+3>=0; x-1>=0|] diff --git a/tests/results/0500_loop_count.constants.txt b/tests/results/0500_loop_count.constants.txt new file mode 100644 index 0000000..530df33 --- /dev/null +++ b/tests/results/0500_loop_count.constants.txt @@ -0,0 +1,5 @@ +sources/0500_loop_count.c:3.2-4.2: [ x in {0} ] +sources/0500_loop_count.c:3.2-4.2: [ x in {1} ] +sources/0500_loop_count.c:3.2-4.2: [ x in {2} ] +sources/0500_loop_count.c:3.2-4.2: [ x in top ] +Output: [ x in top ] diff --git a/tests/results/0500_loop_count.intervals.txt b/tests/results/0500_loop_count.intervals.txt new file mode 100644 index 0000000..ed48d45 --- /dev/null +++ b/tests/results/0500_loop_count.intervals.txt @@ -0,0 +1,5 @@ +sources/0500_loop_count.c:3.2-4.2: [ x in [0;0] ] +sources/0500_loop_count.c:3.2-4.2: [ x in [1;1] ] +sources/0500_loop_count.c:3.2-4.2: [ x in [2;2] ] +sources/0500_loop_count.c:3.2-4.2: [ x in [3;99] ] +Output: [ x in [100;100] ] diff --git a/tests/results/0500_loop_count.polyhedra.txt b/tests/results/0500_loop_count.polyhedra.txt new file mode 100644 index 0000000..effcc42 --- /dev/null +++ b/tests/results/0500_loop_count.polyhedra.txt @@ -0,0 +1,5 @@ +sources/0500_loop_count.c:3.2-4.2: [|x=0|] +sources/0500_loop_count.c:3.2-4.2: [|x-1=0|] +sources/0500_loop_count.c:3.2-4.2: [|x-2=0|] +sources/0500_loop_count.c:3.2-4.2: [|-x+99>=0; x-3>=0|] +Output: [|x-100=0|] diff --git a/tests/results/0501_loop_infinite.constants.txt b/tests/results/0501_loop_infinite.constants.txt new file mode 100644 index 0000000..e0eb2c9 --- /dev/null +++ b/tests/results/0501_loop_infinite.constants.txt @@ -0,0 +1,5 @@ +sources/0501_loop_infinite.c:3.2-4.0: [ x in {0} ] +sources/0501_loop_infinite.c:3.2-4.0: [ x in {0} ] +sources/0501_loop_infinite.c:3.2-4.0: [ x in {0} ] +sources/0501_loop_infinite.c:3.2-4.0: [ x in {0} ] +Output: bottom diff --git a/tests/results/0501_loop_infinite.intervals.txt b/tests/results/0501_loop_infinite.intervals.txt new file mode 100644 index 0000000..eab060c --- /dev/null +++ b/tests/results/0501_loop_infinite.intervals.txt @@ -0,0 +1,5 @@ +sources/0501_loop_infinite.c:3.2-4.0: [ x in [0;0] ] +sources/0501_loop_infinite.c:3.2-4.0: [ x in [0;0] ] +sources/0501_loop_infinite.c:3.2-4.0: [ x in [0;0] ] +sources/0501_loop_infinite.c:3.2-4.0: [ x in [0;0] ] +Output: bottom diff --git a/tests/results/0501_loop_infinite.polyhedra.txt b/tests/results/0501_loop_infinite.polyhedra.txt new file mode 100644 index 0000000..64d2853 --- /dev/null +++ b/tests/results/0501_loop_infinite.polyhedra.txt @@ -0,0 +1,5 @@ +sources/0501_loop_infinite.c:3.2-4.0: [|x=0|] +sources/0501_loop_infinite.c:3.2-4.0: [|x=0|] +sources/0501_loop_infinite.c:3.2-4.0: [|x=0|] +sources/0501_loop_infinite.c:3.2-4.0: [|x=0|] +Output: bottom diff --git a/tests/results/0502_loop_infinite2.constants.txt b/tests/results/0502_loop_infinite2.constants.txt new file mode 100644 index 0000000..015089f --- /dev/null +++ b/tests/results/0502_loop_infinite2.constants.txt @@ -0,0 +1,5 @@ +sources/0502_loop_infinite2.c:3.2-4.2: [ x in {0} ] +sources/0502_loop_infinite2.c:3.2-4.2: [ x in {-1} ] +sources/0502_loop_infinite2.c:3.2-4.2: [ x in {-2} ] +sources/0502_loop_infinite2.c:3.2-4.2: [ x in top ] +Output: [ x in top ] diff --git a/tests/results/0502_loop_infinite2.intervals.txt b/tests/results/0502_loop_infinite2.intervals.txt new file mode 100644 index 0000000..bd8f380 --- /dev/null +++ b/tests/results/0502_loop_infinite2.intervals.txt @@ -0,0 +1,5 @@ +sources/0502_loop_infinite2.c:3.2-4.2: [ x in [0;0] ] +sources/0502_loop_infinite2.c:3.2-4.2: [ x in [-1;-1] ] +sources/0502_loop_infinite2.c:3.2-4.2: [ x in [-2;-2] ] +sources/0502_loop_infinite2.c:3.2-4.2: [ x in [-oo;-3] ] +Output: bottom diff --git a/tests/results/0502_loop_infinite2.polyhedra.txt b/tests/results/0502_loop_infinite2.polyhedra.txt new file mode 100644 index 0000000..41c8ebb --- /dev/null +++ b/tests/results/0502_loop_infinite2.polyhedra.txt @@ -0,0 +1,5 @@ +sources/0502_loop_infinite2.c:3.2-4.2: [|x=0|] +sources/0502_loop_infinite2.c:3.2-4.2: [|x+1=0|] +sources/0502_loop_infinite2.c:3.2-4.2: [|x+2=0|] +sources/0502_loop_infinite2.c:3.2-4.2: [|-x-3>=0|] +Output: bottom diff --git a/tests/results/0503_loop_nondet.constants.txt b/tests/results/0503_loop_nondet.constants.txt new file mode 100644 index 0000000..1002f30 --- /dev/null +++ b/tests/results/0503_loop_nondet.constants.txt @@ -0,0 +1,5 @@ +sources/0503_loop_nondet.c:3.2-4.2: [ x in {0} ] +sources/0503_loop_nondet.c:3.2-4.2: [ x in {1} ] +sources/0503_loop_nondet.c:3.2-4.2: [ x in {2} ] +sources/0503_loop_nondet.c:3.2-4.2: [ x in top ] +Output: [ x in top ] diff --git a/tests/results/0503_loop_nondet.intervals.txt b/tests/results/0503_loop_nondet.intervals.txt new file mode 100644 index 0000000..b4af6d2 --- /dev/null +++ b/tests/results/0503_loop_nondet.intervals.txt @@ -0,0 +1,5 @@ +sources/0503_loop_nondet.c:3.2-4.2: [ x in [0;0] ] +sources/0503_loop_nondet.c:3.2-4.2: [ x in [1;1] ] +sources/0503_loop_nondet.c:3.2-4.2: [ x in [2;2] ] +sources/0503_loop_nondet.c:3.2-4.2: [ x in [3;+oo] ] +Output: [ x in [0;+oo] ] diff --git a/tests/results/0503_loop_nondet.polyhedra.txt b/tests/results/0503_loop_nondet.polyhedra.txt new file mode 100644 index 0000000..a358809 --- /dev/null +++ b/tests/results/0503_loop_nondet.polyhedra.txt @@ -0,0 +1,5 @@ +sources/0503_loop_nondet.c:3.2-4.2: [|x=0|] +sources/0503_loop_nondet.c:3.2-4.2: [|x-1=0|] +sources/0503_loop_nondet.c:3.2-4.2: [|x-2=0|] +sources/0503_loop_nondet.c:3.2-4.2: [|x-3>=0|] +Output: [|x>=0|] diff --git a/tests/results/0504_loop_rel.constants.txt b/tests/results/0504_loop_rel.constants.txt new file mode 100644 index 0000000..e3ca5e3 --- /dev/null +++ b/tests/results/0504_loop_rel.constants.txt @@ -0,0 +1,6 @@ +sources/0504_loop_rel.c:4.2-5.2: [ x in {0}, N in top ] +sources/0504_loop_rel.c:4.2-5.2: [ x in {1}, N in top ] +sources/0504_loop_rel.c:4.2-5.2: [ x in {2}, N in top ] +sources/0504_loop_rel.c:4.2-5.2: [ x in top, N in top ] +sources/0504_loop_rel.c:7.0-13: ERROR: assertion failure +Output: [ N in top, x in top ] diff --git a/tests/results/0504_loop_rel.intervals.txt b/tests/results/0504_loop_rel.intervals.txt new file mode 100644 index 0000000..2f0c86c --- /dev/null +++ b/tests/results/0504_loop_rel.intervals.txt @@ -0,0 +1,6 @@ +sources/0504_loop_rel.c:4.2-5.2: [ x in [0;0], N in [1;1000] ] +sources/0504_loop_rel.c:4.2-5.2: [ x in [1;1], N in [2;1000] ] +sources/0504_loop_rel.c:4.2-5.2: [ x in [2;2], N in [3;1000] ] +sources/0504_loop_rel.c:4.2-5.2: [ x in [3;999], N in [4;1000] ] +sources/0504_loop_rel.c:7.0-13: ERROR: assertion failure +Output: [ N in [0;1000], x in [0;1000] ] diff --git a/tests/results/0504_loop_rel.polyhedra.txt b/tests/results/0504_loop_rel.polyhedra.txt new file mode 100644 index 0000000..5d3d189 --- /dev/null +++ b/tests/results/0504_loop_rel.polyhedra.txt @@ -0,0 +1,5 @@ +sources/0504_loop_rel.c:4.2-5.2: [|x=0; -N+1000>=0; N-1>=0|] +sources/0504_loop_rel.c:4.2-5.2: [|x-1=0; -N+1000>=0; N-2>=0|] +sources/0504_loop_rel.c:4.2-5.2: [|x-2=0; -N+1000>=0; N-3>=0|] +sources/0504_loop_rel.c:4.2-5.2: [|-N+1000>=0; x-3>=0; N-x-1>=0|] +Output: [|-N+x=0; -N+1000>=0; N>=0|] diff --git a/tests/results/0505_loop_rel2.constants.txt b/tests/results/0505_loop_rel2.constants.txt new file mode 100644 index 0000000..762a610 --- /dev/null +++ b/tests/results/0505_loop_rel2.constants.txt @@ -0,0 +1,6 @@ +sources/0505_loop_rel2.c:4.2-5.2: [ x in {0}, N in top ] +sources/0505_loop_rel2.c:4.2-5.2: [ x in top, N in top ] +sources/0505_loop_rel2.c:4.2-5.2: [ x in top, N in top ] +sources/0505_loop_rel2.c:4.2-5.2: [ x in top, N in top ] +sources/0505_loop_rel2.c:7.0-22: ERROR: assertion failure +Output: [ N in top, x in top ] diff --git a/tests/results/0505_loop_rel2.intervals.txt b/tests/results/0505_loop_rel2.intervals.txt new file mode 100644 index 0000000..f1e9597 --- /dev/null +++ b/tests/results/0505_loop_rel2.intervals.txt @@ -0,0 +1,6 @@ +sources/0505_loop_rel2.c:4.2-5.2: [ x in [0;0], N in [1;1000] ] +sources/0505_loop_rel2.c:4.2-5.2: [ x in [0;3], N in [1;1000] ] +sources/0505_loop_rel2.c:4.2-5.2: [ x in [0;6], N in [1;1000] ] +sources/0505_loop_rel2.c:4.2-5.2: [ x in [0;999], N in [1;1000] ] +sources/0505_loop_rel2.c:7.0-22: ERROR: assertion failure +Output: [ N in [0;1000], x in [0;1002] ] diff --git a/tests/results/0505_loop_rel2.polyhedra.txt b/tests/results/0505_loop_rel2.polyhedra.txt new file mode 100644 index 0000000..cf93640 --- /dev/null +++ b/tests/results/0505_loop_rel2.polyhedra.txt @@ -0,0 +1,5 @@ +sources/0505_loop_rel2.c:4.2-5.2: [|x=0; -N+1000>=0; N-1>=0|] +sources/0505_loop_rel2.c:4.2-5.2: [|-N+1000>=0; -x+3>=0; x>=0; N-x-1>=0|] +sources/0505_loop_rel2.c:4.2-5.2: [|-N+1000>=0; -x+6>=0; x>=0; N-x-1>=0|] +sources/0505_loop_rel2.c:4.2-5.2: [|-N+1000>=0; x>=0; N-x-1>=0|] +Output: [|-N+1000>=0; -N+x>=0; N-x+2>=0; 3N-x>=0|] diff --git a/tests/results/0506_loop_limit.constants.txt b/tests/results/0506_loop_limit.constants.txt new file mode 100644 index 0000000..39f5f34 --- /dev/null +++ b/tests/results/0506_loop_limit.constants.txt @@ -0,0 +1,2 @@ +sources/0506_loop_limit.c:5.0-9: [ x in top ] +Output: [ x in top ] diff --git a/tests/results/0506_loop_limit.intervals.txt b/tests/results/0506_loop_limit.intervals.txt new file mode 100644 index 0000000..7cb2cef --- /dev/null +++ b/tests/results/0506_loop_limit.intervals.txt @@ -0,0 +1,2 @@ +sources/0506_loop_limit.c:5.0-9: [ x in [0;+oo] ] +Output: [ x in [0;+oo] ] diff --git a/tests/results/0506_loop_limit.polyhedra.txt b/tests/results/0506_loop_limit.polyhedra.txt new file mode 100644 index 0000000..4577a55 --- /dev/null +++ b/tests/results/0506_loop_limit.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0506_loop_limit.c:5.0-9: [|x>=0|] +Output: [|x>=0|] diff --git a/tests/results/0507_loop_limit2.constants.txt b/tests/results/0507_loop_limit2.constants.txt new file mode 100644 index 0000000..b3c5933 --- /dev/null +++ b/tests/results/0507_loop_limit2.constants.txt @@ -0,0 +1,2 @@ +sources/0507_loop_limit2.c:6.0-9: [ x in top ] +Output: [ N in top, x in top ] diff --git a/tests/results/0507_loop_limit2.intervals.txt b/tests/results/0507_loop_limit2.intervals.txt new file mode 100644 index 0000000..738b69b --- /dev/null +++ b/tests/results/0507_loop_limit2.intervals.txt @@ -0,0 +1,2 @@ +sources/0507_loop_limit2.c:6.0-9: [ x in [0;+oo] ] +Output: [ N in [0;1000], x in [0;+oo] ] diff --git a/tests/results/0507_loop_limit2.polyhedra.txt b/tests/results/0507_loop_limit2.polyhedra.txt new file mode 100644 index 0000000..d2a1ea6 --- /dev/null +++ b/tests/results/0507_loop_limit2.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0507_loop_limit2.c:6.0-9: [|-x+1000>=0; x>=0|] +Output: [|-N+1000>=0; x>=0; N-x>=0|] diff --git a/tests/results/0508_loop_init.constants.txt b/tests/results/0508_loop_init.constants.txt new file mode 100644 index 0000000..702e551 --- /dev/null +++ b/tests/results/0508_loop_init.constants.txt @@ -0,0 +1,2 @@ +sources/0508_loop_init.c:13.2-14.0: ERROR: assertion failure +Output: [ init in top, x in top ] diff --git a/tests/results/0508_loop_init.intervals.txt b/tests/results/0508_loop_init.intervals.txt new file mode 100644 index 0000000..c52a9a1 --- /dev/null +++ b/tests/results/0508_loop_init.intervals.txt @@ -0,0 +1 @@ +Output: [ init in [0;1], x in [-oo;+oo] ] diff --git a/tests/results/0508_loop_init.polyhedra.txt b/tests/results/0508_loop_init.polyhedra.txt new file mode 100644 index 0000000..4b8711f --- /dev/null +++ b/tests/results/0508_loop_init.polyhedra.txt @@ -0,0 +1 @@ +Output: [|-init+1>=0; init>=0|] diff --git a/tests/results/0509_loop_nested.constants.txt b/tests/results/0509_loop_nested.constants.txt new file mode 100644 index 0000000..cbca9fb --- /dev/null +++ b/tests/results/0509_loop_nested.constants.txt @@ -0,0 +1 @@ +Output: [ i in top, j in top ] diff --git a/tests/results/0509_loop_nested.intervals.txt b/tests/results/0509_loop_nested.intervals.txt new file mode 100644 index 0000000..c8ba912 --- /dev/null +++ b/tests/results/0509_loop_nested.intervals.txt @@ -0,0 +1 @@ +Output: [ i in [1000;1000], j in [2;999] ] diff --git a/tests/results/0509_loop_nested.polyhedra.txt b/tests/results/0509_loop_nested.polyhedra.txt new file mode 100644 index 0000000..f00ac71 --- /dev/null +++ b/tests/results/0509_loop_nested.polyhedra.txt @@ -0,0 +1 @@ +Output: [|j-999=0; i-1000=0|] diff --git a/tests/results/0510_loop_nested2.constants.txt b/tests/results/0510_loop_nested2.constants.txt new file mode 100644 index 0000000..cbca9fb --- /dev/null +++ b/tests/results/0510_loop_nested2.constants.txt @@ -0,0 +1 @@ +Output: [ i in top, j in top ] diff --git a/tests/results/0510_loop_nested2.intervals.txt b/tests/results/0510_loop_nested2.intervals.txt new file mode 100644 index 0000000..c8ba912 --- /dev/null +++ b/tests/results/0510_loop_nested2.intervals.txt @@ -0,0 +1 @@ +Output: [ i in [1000;1000], j in [2;999] ] diff --git a/tests/results/0510_loop_nested2.polyhedra.txt b/tests/results/0510_loop_nested2.polyhedra.txt new file mode 100644 index 0000000..f00ac71 --- /dev/null +++ b/tests/results/0510_loop_nested2.polyhedra.txt @@ -0,0 +1 @@ +Output: [|j-999=0; i-1000=0|] diff --git a/tests/results/0600_bubble_sort.constants.txt b/tests/results/0600_bubble_sort.constants.txt new file mode 100644 index 0000000..2a0bcda --- /dev/null +++ b/tests/results/0600_bubble_sort.constants.txt @@ -0,0 +1,33 @@ +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +Output: [ B in top, J in top, N in top, T in top ] diff --git a/tests/results/0600_bubble_sort.intervals.txt b/tests/results/0600_bubble_sort.intervals.txt new file mode 100644 index 0000000..7357141 --- /dev/null +++ b/tests/results/0600_bubble_sort.intervals.txt @@ -0,0 +1,25 @@ +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +Output: [ B in [0;0], J in [-oo;+oo], N in [0;100000], T in [-oo;+oo] ] diff --git a/tests/results/0600_bubble_sort.polyhedra.txt b/tests/results/0600_bubble_sort.polyhedra.txt new file mode 100644 index 0000000..e2a1918 --- /dev/null +++ b/tests/results/0600_bubble_sort.polyhedra.txt @@ -0,0 +1 @@ +Output: [|B=0; -N+100000>=0; N>=0|] diff --git a/tests/results/0601_heap_sort.constants.txt b/tests/results/0601_heap_sort.constants.txt new file mode 100644 index 0000000..3f8cad1 --- /dev/null +++ b/tests/results/0601_heap_sort.constants.txt @@ -0,0 +1,104 @@ +sources/0601_heap_sort.c:17.2-18.0: ERROR: assertion failure +sources/0601_heap_sort.c:21.3-22.3: ERROR: assertion failure +sources/0601_heap_sort.c:22.3-23.3: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +sources/0601_heap_sort.c:60.4-61.4: ERROR: assertion failure +sources/0601_heap_sort.c:65.2-66.0: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +sources/0601_heap_sort.c:60.4-61.4: ERROR: assertion failure +sources/0601_heap_sort.c:65.2-66.0: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +sources/0601_heap_sort.c:60.4-61.4: ERROR: assertion failure +sources/0601_heap_sort.c:65.2-66.0: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +sources/0601_heap_sort.c:60.4-61.4: ERROR: assertion failure +sources/0601_heap_sort.c:65.2-66.0: ERROR: assertion failure +Output: [ I in top, J in top, L in top, N in top, R in top ] diff --git a/tests/results/0601_heap_sort.intervals.txt b/tests/results/0601_heap_sort.intervals.txt new file mode 100644 index 0000000..e8ec3f7 --- /dev/null +++ b/tests/results/0601_heap_sort.intervals.txt @@ -0,0 +1,95 @@ +sources/0601_heap_sort.c:17.2-18.0: ERROR: assertion failure +sources/0601_heap_sort.c:21.3-22.3: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +Output: [ I in [-oo;+oo], J in [-oo;+oo], L in [-oo;100000], N in [1;100000], R in [0;1] ] diff --git a/tests/results/0601_heap_sort.polyhedra.txt b/tests/results/0601_heap_sort.polyhedra.txt new file mode 100644 index 0000000..6dde246 --- /dev/null +++ b/tests/results/0601_heap_sort.polyhedra.txt @@ -0,0 +1 @@ +Output: [|-99999L+49999R+99999>=0; -2L+N+1>=0; -R+1>=0; L-1>=0|] diff --git a/tests/results/0602_rate_limiter.constants.txt b/tests/results/0602_rate_limiter.constants.txt new file mode 100644 index 0000000..e0768fb --- /dev/null +++ b/tests/results/0602_rate_limiter.constants.txt @@ -0,0 +1,2 @@ +sources/0602_rate_limiter.c:26.0-30: ERROR: assertion failure +Output: [ D in top, S in top, X in top, Y in top ] diff --git a/tests/results/0602_rate_limiter.intervals.txt b/tests/results/0602_rate_limiter.intervals.txt new file mode 100644 index 0000000..56f35e9 --- /dev/null +++ b/tests/results/0602_rate_limiter.intervals.txt @@ -0,0 +1,2 @@ +sources/0602_rate_limiter.c:26.0-30: ERROR: assertion failure +Output: [ D in [-oo;+oo], S in [-oo;+oo], X in [-oo;+oo], Y in [-128;128] ] diff --git a/tests/results/0602_rate_limiter.polyhedra.txt b/tests/results/0602_rate_limiter.polyhedra.txt new file mode 100644 index 0000000..b4c3d72 --- /dev/null +++ b/tests/results/0602_rate_limiter.polyhedra.txt @@ -0,0 +1,2 @@ +sources/0602_rate_limiter.c:26.0-30: ERROR: assertion failure +Output: [|-Y+128>=0; Y+128>=0|] diff --git a/tests/results/0603_rate_limiter2.constants.txt b/tests/results/0603_rate_limiter2.constants.txt new file mode 100644 index 0000000..de62fd6 --- /dev/null +++ b/tests/results/0603_rate_limiter2.constants.txt @@ -0,0 +1,5 @@ +sources/0603_rate_limiter2.c:20.2-21.0: ERROR: assertion failure +sources/0603_rate_limiter2.c:20.2-21.0: ERROR: assertion failure +sources/0603_rate_limiter2.c:20.2-21.0: ERROR: assertion failure +sources/0603_rate_limiter2.c:20.2-21.0: ERROR: assertion failure +Output: [ D in top, S in top, X in top, Y in top ] diff --git a/tests/results/0603_rate_limiter2.intervals.txt b/tests/results/0603_rate_limiter2.intervals.txt new file mode 100644 index 0000000..3c3ed17 --- /dev/null +++ b/tests/results/0603_rate_limiter2.intervals.txt @@ -0,0 +1,4 @@ +sources/0603_rate_limiter2.c:20.2-21.0: ERROR: assertion failure +sources/0603_rate_limiter2.c:20.2-21.0: ERROR: assertion failure +sources/0603_rate_limiter2.c:20.2-21.0: ERROR: assertion failure +Output: [ D in [-oo;+oo], S in [-oo;+oo], X in [-oo;+oo], Y in [-128;128] ] diff --git a/tests/results/0603_rate_limiter2.polyhedra.txt b/tests/results/0603_rate_limiter2.polyhedra.txt new file mode 100644 index 0000000..13697f6 --- /dev/null +++ b/tests/results/0603_rate_limiter2.polyhedra.txt @@ -0,0 +1 @@ +Output: [|-Y+128>=0; Y+128>=0|] diff --git a/tests/results/all.constants.txt b/tests/results/all.constants.txt new file mode 100644 index 0000000..ac3ee3f --- /dev/null +++ b/tests/results/all.constants.txt @@ -0,0 +1,1135 @@ +sources/0000_noinit_var.c + + 1 int x; + +Output: [ x in top ] + +------------------------------------- + +sources/0001_noinit_2var.c + + 1 int x; + 2 int y; + +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0002_init_var.c + + 1 int x = 0; + +Output: [ x in {0} ] + +------------------------------------- + +sources/0003_init_2var.c + + 1 int x = 0; + 2 int y = 1; + +Output: [ x in {0}, y in {1} ] + +------------------------------------- + +sources/0004_init_2var2.c + + 1 int x = 9, y = 12; + +Output: [ x in {9}, y in {12} ] + +------------------------------------- + +sources/0100_print_var.c + + 1 int x = 2; + 2 print(x); + +sources/0100_print_var.c:2.0-9: [ x in {2} ] +Output: [ x in {2} ] + +------------------------------------- + +sources/0101_print_2var.c + + 1 int x = 3; + 2 int y = 15; + 3 print(y); + +sources/0101_print_2var.c:3.0-9: [ y in {15} ] +Output: [ x in {3}, y in {15} ] + +------------------------------------- + +sources/0102_print_3var.c + + 1 int x = 3; + 2 int y = 15; + 3 int z = 99; + 4 print(z,x); + +sources/0102_print_3var.c:4.0-11: [ z in {99}, x in {3} ] +Output: [ x in {3}, y in {15}, z in {99} ] + +------------------------------------- + +sources/0103_local.c + + 1 int x = 12; + 2 { + 3 int y = 9; + 4 print(x,y); + 5 } + +sources/0103_local.c:4.2-5.0: [ x in {12}, y in {9} ] +Output: [ x in {12} ] + +------------------------------------- + +sources/0200_assign_cst.c + + 1 int x; + 2 print(x); + 3 x = 12; + 4 print(x); + 5 x = 15; + 6 print(x); + +sources/0200_assign_cst.c:2.0-9: [ x in top ] +sources/0200_assign_cst.c:4.0-9: [ x in {12} ] +sources/0200_assign_cst.c:6.0-9: [ x in {15} ] +Output: [ x in {15} ] + +------------------------------------- + +sources/0201_assign_cst2.c + + 1 int x, y; + 2 print(x,y); + 3 x = 12; + 4 print(x,y); + 5 y = 15; + 6 x = 99; + 7 print(x,y); + +sources/0201_assign_cst2.c:2.0-11: [ x in top, y in top ] +sources/0201_assign_cst2.c:4.0-11: [ x in {12}, y in top ] +sources/0201_assign_cst2.c:7.0-11: [ x in {99}, y in {15} ] +Output: [ x in {99}, y in {15} ] + +------------------------------------- + +sources/0202_assign_expr.c + + 1 int x; + 2 x = 2 + 2; + +Output: [ x in {4} ] + +------------------------------------- + +sources/0203_assign_expr2.c + + 1 int x,y; + 2 x = 12; + 3 y = 16; + 4 x = x + y + 2; + 5 print(x); + +sources/0203_assign_expr2.c:5.0-9: [ x in {30} ] +Output: [ x in {30}, y in {16} ] + +------------------------------------- + +sources/0204_assign_rand.c + + 1 int x; + 2 x = rand(1,99); + 3 print(x); + +sources/0204_assign_rand.c:3.0-9: [ x in top ] +Output: [ x in top ] + +------------------------------------- + +sources/0205_assign_rand2.c + + 1 int x; + 2 x = rand(10,-5); + 3 print(x); + +sources/0205_assign_rand2.c:3.0-9: bottom +Output: bottom + +------------------------------------- + +sources/0206_assign_add.c + + 1 int x; + 2 x = 2 + 5; + +Output: [ x in {7} ] + +------------------------------------- + +sources/0207_assign_add2.c + + 1 int x; + 2 x = rand(1,5) + rand (10,10); + +Output: [ x in top ] + +------------------------------------- + +sources/0208_assign_add3.c + + 1 int x; + 2 x = x + 2; + +Output: [ x in top ] + +------------------------------------- + +sources/0209_assign_neg.c + + 1 int x; + 2 x = -9; + +Output: [ x in {-9} ] + +------------------------------------- + +sources/0210_assign_neg2.c + + 1 int x; + 2 x = -rand(-1,10); + 3 + +Output: [ x in top ] + +------------------------------------- + +sources/0211_assign_sub.c + + 1 int x; + 2 x = 999 - 1; + +Output: [ x in {998} ] + +------------------------------------- + +sources/0212_assign_sub2.c + + 1 int x; + 2 x = rand(1,10) - rand(2,3); + +Output: [ x in top ] + +------------------------------------- + +sources/0213_assign_mul.c + + 1 int x; + 2 x = 5 * 8; + +Output: [ x in {40} ] + +------------------------------------- + +sources/0214_assign_mul2.c + + 1 int x; + 2 x = rand(1,3) * rand(2,9); + +Output: [ x in top ] + +------------------------------------- + +sources/0215_assign_mul3.c + + 1 int x; + 2 x = rand(-5,3) * rand(-1,10); + +Output: [ x in top ] + +------------------------------------- + +sources/0216_assign_mul4.c + + 1 int x; + 2 x = x * 0; + +Output: [ x in {0} ] + +------------------------------------- + +sources/0217_assign_copy.c + + 1 int x; + 2 int y; + 3 x = 12; + 4 y = x; + 5 print(y); + +sources/0217_assign_copy.c:5.0-9: [ y in {12} ] +Output: [ x in {12}, y in {12} ] + +------------------------------------- + +sources/0218_assign_rel.c + + 1 int x; + 2 int y; + 3 x = 15; + 4 y = x + 2; + 5 print(y); + +sources/0218_assign_rel.c:5.0-9: [ y in {17} ] +Output: [ x in {15}, y in {17} ] + +------------------------------------- + +sources/0219_assign_rel2.c + + 1 int x = rand(1,5); + 2 int y = rand(2,10); + 3 int z = x + 2*y; + +Output: [ x in top, y in top, z in top ] + +------------------------------------- + +sources/0300_if_true.c + + 1 int x = 1; + 2 if (1 <= 2) x = 9; + +Output: [ x in {9} ] + +------------------------------------- + +sources/0301_if_false.c + + 1 int x = 1; + 2 if (1 >= 2) x = 9; + +Output: [ x in {1} ] + +------------------------------------- + +sources/0302_if_both.c + + 1 int x = 1; + 2 if (rand(0,1) == 0) x = 9; + +Output: [ x in top ] + +------------------------------------- + +sources/0303_if_else_true.c + + 1 int x = 1; + 2 if (1 <= 2) x = 5; else x = 10; + +Output: [ x in {5} ] + +------------------------------------- + +sources/0304_if_else_false.c + + 1 int x = 1; + 2 if (1 >= 2) x = 5; else x = 10; + +Output: [ x in {10} ] + +------------------------------------- + +sources/0305_if_else_both.c + + 1 int x = 1; + 2 if (rand(0,1) == 0) x = 5; else x = 10; + +Output: [ x in top ] + +------------------------------------- + +sources/0306_if_rel.c + + 1 int x,y; + 2 if (rand(0,1) == 0) { x = 1; y = 3; } + 3 else { x = 2; y = 1; } + +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0307_if_var.c + + 1 int x = rand(-10,20); + 2 if (x >= 0) { print(x); } + 3 else { print(x); } + +sources/0307_if_var.c:2.14-24: [ x in top ] +sources/0307_if_var.c:3.7-17: [ x in top ] +Output: [ x in top ] + +------------------------------------- + +sources/0308_if_var2.c + + 1 int x = rand(-20,10); + 2 if (x < 2) x = -x; + +Output: [ x in top ] + +------------------------------------- + +sources/0309_if_var_rel.c + + 1 int x = rand(-10,25); + 2 int y = rand(-15,20); + 3 if (x >= y) x = y; + +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0310_cmp_le.c + + 1 int x = rand(10,20); + 2 int y = rand(15,30); + 3 if (x <= y) print(x,y); + +sources/0310_cmp_le.c:3.11-23: [ x in top, y in top ] +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0311_cmp_le2.c + + 1 int x = rand(10,20); + 2 int y = rand(8,17); + 3 if (x <= y) print(x,y); + +sources/0311_cmp_le2.c:3.11-23: [ x in top, y in top ] +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0312_cmp_le3.c + + 1 int y = rand(10,20); + 2 int x = rand(30,55); + 3 if (x <= y) print(x); + +sources/0312_cmp_le3.c:3.11-21: [ x in top ] +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0313_cmp_lt.c + + 1 int x = rand(10,20); + 2 int y = rand(5,15); + 3 if (x < y) print(x,y); + +sources/0313_cmp_lt.c:3.10-22: [ x in top, y in top ] +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0314_cmp_ge.c + + 1 int x = rand(10,20); + 2 int y = rand(15,30); + 3 if (x >= y) print(x,y); + +sources/0314_cmp_ge.c:3.11-23: [ x in top, y in top ] +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0315_cmp_gt.c + + 1 int x = rand(10,20); + 2 int y = rand(15,30); + 3 if (x > y) print(x,y); + +sources/0315_cmp_gt.c:3.10-22: [ x in top, y in top ] +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0316_cmp_eq.c + + 1 int x = rand(15,30); + 2 int y = rand(10,20); + 3 if (x == y) print(x,y); + +sources/0316_cmp_eq.c:3.11-23: [ x in top, y in top ] +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0317_cmp_eq2.c + + 1 int x = rand(15,20); + 2 int y = rand(25,30); + 3 if (x == y) print(x,y); + +sources/0317_cmp_eq2.c:3.11-23: [ x in top, y in top ] +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0318_cmp_ne.c + + 1 int x = rand(10,15); + 2 int y = rand(10,15); + 3 if (x != y) print(x,y); + +sources/0318_cmp_ne.c:3.11-23: [ x in top, y in top ] +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0319_cmp_ne.c + + 1 int x = rand(10,15); + 2 int y = 10; + 3 if (x != y) print(x,y); + +sources/0319_cmp_ne.c:3.11-23: [ x in top, y in {10} ] +Output: [ x in top, y in {10} ] + +------------------------------------- + +sources/0320_cmp_eq_ne.c + + 1 int x = rand(10,15); + 2 int y = 10; + 3 if (x == y) print(x,y); + 4 else print(x,y); + 5 + +sources/0320_cmp_eq_ne.c:3.11-4.0: [ x in {10}, y in {10} ] +sources/0320_cmp_eq_ne.c:4.4-16: [ x in top, y in {10} ] +Output: [ x in top, y in {10} ] + +------------------------------------- + +sources/0321_cmp_rel.c + + 1 int x = rand(10,20); + 2 int y = x; + 3 if (x >= 15) { print(y); } + +sources/0321_cmp_rel.c:3.15-25: [ y in top ] +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0322_if_and.c + + 1 int x = rand(10,20); + 2 int y = rand(30,40); + 3 if (x>=15 && y>=35) { print(x,y); } + 4 else { print(x,y); } + +sources/0322_if_and.c:3.22-34: [ x in top, y in top ] +sources/0322_if_and.c:4.7-19: [ x in top, y in top ] +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0323_if_or.c + + 1 int x = rand(10,20); + 2 int y = rand(30,40); + 3 if (x>=15 || y>=35) { print(x,y); } + 4 else { print(x,y); } + +sources/0323_if_or.c:3.22-34: [ x in top, y in top ] +sources/0323_if_or.c:4.7-19: [ x in top, y in top ] +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0324_if_not.c + + 1 int x = rand(10,20); + 2 int y = rand(30,40); + 3 if (!(x>=15) || y>=35) { print(x,y); } + 4 else { print(x,y); } + +sources/0324_if_not.c:3.25-37: [ x in top, y in top ] +sources/0324_if_not.c:4.7-19: [ x in top, y in top ] +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0325_if_bool.c + + 1 int x = rand(10,20); + 2 int y = rand(10,20); + 3 if (x<=15 && y>=15 || x>=15 && y<=15) { print(x,y); } + 4 else { print(x,y); } + +sources/0325_if_bool.c:3.40-52: [ x in top, y in top ] +sources/0325_if_bool.c:4.7-19: [ x in top, y in top ] +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0400_assert_true.c + + 1 int x = 2; + 2 assert(x>=1); + +Output: [ x in {2} ] + +------------------------------------- + +sources/0401_assert_false.c + + 1 int x = 9; + 2 assert (x < 5); + +sources/0401_assert_false.c:2.0-15: ERROR: assertion failure +Output: bottom + +------------------------------------- + +sources/0402_assert_both.c + + 1 int x = rand (-5,10); + 2 assert(x >= 0); + 3 assert(x > 0); + 4 + +sources/0402_assert_both.c:2.0-15: ERROR: assertion failure +sources/0402_assert_both.c:3.0-14: ERROR: assertion failure +Output: [ x in top ] + +------------------------------------- + +sources/0403_assert_both2.c + + 1 int x = rand (-5,10); + 2 assert(x > 0); + 3 assert(x >= 0); + +sources/0403_assert_both2.c:2.0-14: ERROR: assertion failure +sources/0403_assert_both2.c:3.0-15: ERROR: assertion failure +Output: [ x in top ] + +------------------------------------- + +sources/0404_assert_rel.c + + 1 int x,y; + 2 if (rand(0,1)==0) { x = 1; y = 1; } + 3 else { x = 3 ; y = 3; } + 4 assert(x==y); + +sources/0404_assert_rel.c:4.0-13: ERROR: assertion failure +Output: [ x in top, y in top ] + +------------------------------------- + +sources/0500_loop_count.c + + 1 int x = 0; + 2 while (x < 100) { + 3 print(x); + 4 x = x + 1; + 5 } + +sources/0500_loop_count.c:3.2-4.2: [ x in {0} ] +sources/0500_loop_count.c:3.2-4.2: [ x in {1} ] +sources/0500_loop_count.c:3.2-4.2: [ x in {2} ] +sources/0500_loop_count.c:3.2-4.2: [ x in top ] +Output: [ x in top ] + +------------------------------------- + +sources/0501_loop_infinite.c + + 1 int x = 0; + 2 while (x < 10) { + 3 print(x); + 4 } + +sources/0501_loop_infinite.c:3.2-4.0: [ x in {0} ] +sources/0501_loop_infinite.c:3.2-4.0: [ x in {0} ] +sources/0501_loop_infinite.c:3.2-4.0: [ x in {0} ] +sources/0501_loop_infinite.c:3.2-4.0: [ x in {0} ] +Output: bottom + +------------------------------------- + +sources/0502_loop_infinite2.c + + 1 int x = 0; + 2 while (x < 100) { + 3 print(x); + 4 x = x - 1; + 5 } + +sources/0502_loop_infinite2.c:3.2-4.2: [ x in {0} ] +sources/0502_loop_infinite2.c:3.2-4.2: [ x in {-1} ] +sources/0502_loop_infinite2.c:3.2-4.2: [ x in {-2} ] +sources/0502_loop_infinite2.c:3.2-4.2: [ x in top ] +Output: [ x in top ] + +------------------------------------- + +sources/0503_loop_nondet.c + + 1 int x = 0; + 2 while (rand(0,1) == 0) { + 3 print(x); + 4 x = x + 1; + 5 } + +sources/0503_loop_nondet.c:3.2-4.2: [ x in {0} ] +sources/0503_loop_nondet.c:3.2-4.2: [ x in {1} ] +sources/0503_loop_nondet.c:3.2-4.2: [ x in {2} ] +sources/0503_loop_nondet.c:3.2-4.2: [ x in top ] +Output: [ x in top ] + +------------------------------------- + +sources/0504_loop_rel.c + + 1 int N = rand(0,1000); + 2 int x = 0; + 3 while (x < N) { + 4 print(x,N); + 5 x = x + 1; + 6 } + 7 assert(x==N); + +sources/0504_loop_rel.c:4.2-5.2: [ x in {0}, N in top ] +sources/0504_loop_rel.c:4.2-5.2: [ x in {1}, N in top ] +sources/0504_loop_rel.c:4.2-5.2: [ x in {2}, N in top ] +sources/0504_loop_rel.c:4.2-5.2: [ x in top, N in top ] +sources/0504_loop_rel.c:7.0-13: ERROR: assertion failure +Output: [ N in top, x in top ] + +------------------------------------- + +sources/0505_loop_rel2.c + + 1 int N = rand(0,1000); + 2 int x = 0; + 3 while (x < N) { + 4 print(x,N); + 5 x = x + rand(0,3); + 6 } + 7 assert(x>=N && x<N+3); + +sources/0505_loop_rel2.c:4.2-5.2: [ x in {0}, N in top ] +sources/0505_loop_rel2.c:4.2-5.2: [ x in top, N in top ] +sources/0505_loop_rel2.c:4.2-5.2: [ x in top, N in top ] +sources/0505_loop_rel2.c:4.2-5.2: [ x in top, N in top ] +sources/0505_loop_rel2.c:7.0-22: ERROR: assertion failure +Output: [ N in top, x in top ] + +------------------------------------- + +sources/0506_loop_limit.c + + 1 int x = 0; + 2 while (rand(0,1)==0) { + 3 if (x < 10000) x = x + 1; + 4 } + 5 print(x); + +sources/0506_loop_limit.c:5.0-9: [ x in top ] +Output: [ x in top ] + +------------------------------------- + +sources/0507_loop_limit2.c + + 1 int x = 0; + 2 int N = rand(0,1000); + 3 while (rand(0,1)==0) { + 4 if (x < N) x = x + 1; + 5 } + 6 print(x); + +sources/0507_loop_limit2.c:6.0-9: [ x in top ] +Output: [ N in top, x in top ] + +------------------------------------- + +sources/0508_loop_init.c + + 1 int init; + 2 int x; + 3 + 4 init = 0; + 5 while (rand(0,1)==0) { + 6 if (init == 0) { + 7 x = 0; + 8 init = 1; + 9 } +10 else { +11 x = x + 1; +12 } +13 assert(x >= 0); +14 } + +sources/0508_loop_init.c:13.2-14.0: ERROR: assertion failure +Output: [ init in top, x in top ] + +------------------------------------- + +sources/0509_loop_nested.c + + 1 int i=0, j=0; + 2 + 3 while (i < 1000) { + 4 j = 0; + 5 while (j < i) { + 6 j = j + 1; + 7 } + 8 i = i + 1; + 9 } + +Output: [ i in top, j in top ] + +------------------------------------- + +sources/0510_loop_nested2.c + + 1 int i,j; + 2 + 3 i = 0; + 4 while (i < 1000) { + 5 j = 0; + 6 while (j < i) { + 7 j = j + 1; + 8 } + 9 i = i + 1; +10 } + +Output: [ i in top, j in top ] + +------------------------------------- + +sources/0600_bubble_sort.c + + 1 // Example from Cousot Habwachs POPL 1978 + 2 + 3 // Bubble sort, where array operations are abstracted away + 4 // to get a non-deterministic scalar program + 5 + 6 // expected results: + 7 // - with polyhedra, no assertion failure (proof of absence of array overflow) + 8 // - with intervals, assertion failure + 9 +10 int B,J,T; +11 int N = rand(0,100000); // array size +12 +13 B = N; +14 while (B >= 1) { +15 J = 1; +16 T = 0; +17 while (J <= B-1) { +18 +19 // array bound-check +20 assert(1 <= J && J <= N); +21 assert(1 <= (J+1) && (J+1) <= N); +22 +23 // the non-deterministic test models comparing TAB[J] and TAB[J+1] +24 if (rand(0,1)==0) { +25 // where, we would exchange TAB[J] and TAB[J+1]; +26 T = J; +27 } +28 +29 J = J + 1; +30 } +31 B = T; +32 } + +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +Output: [ B in top, J in top, N in top, T in top ] + +------------------------------------- + +sources/0601_heap_sort.c + + 1 // Example from Cousot Habwachs POPL 1978 + 2 + 3 // Heap sort, where array operations are abstracted away + 4 // to get a non-deterministic scalar program + 5 + 6 // expected results: with polyhedra, no assertion failure + 7 + 8 int L,R,I,J; + 9 int N = rand(1,100000); // array size +10 +11 L = N/2 + 1; +12 R = N; +13 +14 if (L >= 2) { +15 L = L - 1; +16 // model the assignment "K = TAB[L]" +17 assert(1 <= L && L <= N); +18 } +19 else { +20 // model the assignments "K = TAB[R]; TAB[R] = TAB[1]" +21 assert(1 <= R && R <= N); +22 assert(1 <= 1 && 1 <= N); +23 R = R - 1; +24 } +25 +26 while (R >= 2) { +27 I = L; +28 J = 2*I; +29 +30 while (J <= R && rand(0,1)==0) { +31 if (J <= R-1) { +32 // model the comparison "TAB[J] < TAB[J+1]" +33 assert(1 <= J && J <= N); +34 assert(1 <= (J+1) && (J+1) <= N); +35 if (rand(0,1)==0) { J = J + 1; } +36 } +37 +38 // model the comparison "K < TAB[J]" +39 assert(1 <= J && J <= N); +40 if (rand(0,1)==0) { +41 // model the assignment "TAB[I] = TAB[J]" +42 assert(1 <= I && I <= N); +43 assert(1 <= J && J <= N); +44 I = J; +45 J = 2*J; +46 } +47 } +48 +49 // model the assignment "TAB[I] = K" +50 assert(1 <= I && I <= N); +51 +52 if (L >= 2) { +53 L = L - 1; +54 // model the assignment "K = TAB[L]" +55 assert(1 <= L && L <= N); +56 } +57 else { +58 // model the assignments "K = TAB[R]; TAB[R] = TAB[1]" +59 assert(1 <= R && R <= N); +60 assert(1 <= 1 && 1 <= N); +61 R = R - 1; +62 } +63 +64 // model the assignment "TAB[1] = K" +65 assert(1 <= 1 && 1 <= N); +66 } + +sources/0601_heap_sort.c:17.2-18.0: ERROR: assertion failure +sources/0601_heap_sort.c:21.3-22.3: ERROR: assertion failure +sources/0601_heap_sort.c:22.3-23.3: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +sources/0601_heap_sort.c:60.4-61.4: ERROR: assertion failure +sources/0601_heap_sort.c:65.2-66.0: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +sources/0601_heap_sort.c:60.4-61.4: ERROR: assertion failure +sources/0601_heap_sort.c:65.2-66.0: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +sources/0601_heap_sort.c:60.4-61.4: ERROR: assertion failure +sources/0601_heap_sort.c:65.2-66.0: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +sources/0601_heap_sort.c:60.4-61.4: ERROR: assertion failure +sources/0601_heap_sort.c:65.2-66.0: ERROR: assertion failure +Output: [ I in top, J in top, L in top, N in top, R in top ] + +------------------------------------- + +sources/0602_rate_limiter.c + + 1 // Example from Miné HOSC 2006 + 2 + 3 // Rate limiter: at each loop iteration, a new input is fetched (X) and + 4 // a new output (Y) is computed; Y tries to follow X but is limited to + 5 // change no more that a given slope (D) in absolute value + 6 + 7 // To prove that the assertion holds, this version needs the polyhedra + 8 // domain and an unrolling factor of at least 6 + 9 +10 int X; // input +11 int Y; // output +12 int S; // last output +13 int D; // maximum slope; +14 +15 Y = 0; +16 while (rand(0,1)==1) { +17 X = rand(-128,128); +18 D = rand(0,16); +19 S = Y; +20 int R = X - S; // current slope +21 Y = X; +22 if (R <= -D) Y = S - D; // slope too small +23 else if (R >= D) Y = S + D; // slope too large +24 } +25 +26 assert(Y >= -128 && Y <= 128); + +sources/0602_rate_limiter.c:26.0-30: ERROR: assertion failure +Output: [ D in top, S in top, X in top, Y in top ] + +------------------------------------- + +sources/0603_rate_limiter2.c + + 1 // This version is similar to the previous one, but the assertion is checked + 2 // inside the loop + 3 // No unrolling is necessary in this version! + 4 + 5 int X; // input + 6 int Y; // output + 7 int S; // last output + 8 int D; // maximum slope; + 9 +10 Y = 0; +11 while (rand(0,1)==1) { +12 X = rand(-128,128); +13 D = rand(0,16); +14 S = Y; +15 int R = X - S; // current slope +16 Y = X; +17 if (R <= -D) Y = S - D; // slope too small +18 else if (R >= D) Y = S + D; // slope too large +19 +20 assert(Y >= -128 && Y <= 128); +21 } + +sources/0603_rate_limiter2.c:20.2-21.0: ERROR: assertion failure +sources/0603_rate_limiter2.c:20.2-21.0: ERROR: assertion failure +sources/0603_rate_limiter2.c:20.2-21.0: ERROR: assertion failure +sources/0603_rate_limiter2.c:20.2-21.0: ERROR: assertion failure +Output: [ D in top, S in top, X in top, Y in top ] + +------------------------------------- + diff --git a/tests/results/all.intervals.txt b/tests/results/all.intervals.txt new file mode 100644 index 0000000..8e7dd94 --- /dev/null +++ b/tests/results/all.intervals.txt @@ -0,0 +1,1115 @@ +sources/0000_noinit_var.c + + 1 int x; + +Output: [ x in [-oo;+oo] ] + +------------------------------------- + +sources/0001_noinit_2var.c + + 1 int x; + 2 int y; + +Output: [ x in [-oo;+oo], y in [-oo;+oo] ] + +------------------------------------- + +sources/0002_init_var.c + + 1 int x = 0; + +Output: [ x in [0;0] ] + +------------------------------------- + +sources/0003_init_2var.c + + 1 int x = 0; + 2 int y = 1; + +Output: [ x in [0;0], y in [1;1] ] + +------------------------------------- + +sources/0004_init_2var2.c + + 1 int x = 9, y = 12; + +Output: [ x in [9;9], y in [12;12] ] + +------------------------------------- + +sources/0100_print_var.c + + 1 int x = 2; + 2 print(x); + +sources/0100_print_var.c:2.0-9: [ x in [2;2] ] +Output: [ x in [2;2] ] + +------------------------------------- + +sources/0101_print_2var.c + + 1 int x = 3; + 2 int y = 15; + 3 print(y); + +sources/0101_print_2var.c:3.0-9: [ y in [15;15] ] +Output: [ x in [3;3], y in [15;15] ] + +------------------------------------- + +sources/0102_print_3var.c + + 1 int x = 3; + 2 int y = 15; + 3 int z = 99; + 4 print(z,x); + +sources/0102_print_3var.c:4.0-11: [ z in [99;99], x in [3;3] ] +Output: [ x in [3;3], y in [15;15], z in [99;99] ] + +------------------------------------- + +sources/0103_local.c + + 1 int x = 12; + 2 { + 3 int y = 9; + 4 print(x,y); + 5 } + +sources/0103_local.c:4.2-5.0: [ x in [12;12], y in [9;9] ] +Output: [ x in [12;12] ] + +------------------------------------- + +sources/0200_assign_cst.c + + 1 int x; + 2 print(x); + 3 x = 12; + 4 print(x); + 5 x = 15; + 6 print(x); + +sources/0200_assign_cst.c:2.0-9: [ x in [-oo;+oo] ] +sources/0200_assign_cst.c:4.0-9: [ x in [12;12] ] +sources/0200_assign_cst.c:6.0-9: [ x in [15;15] ] +Output: [ x in [15;15] ] + +------------------------------------- + +sources/0201_assign_cst2.c + + 1 int x, y; + 2 print(x,y); + 3 x = 12; + 4 print(x,y); + 5 y = 15; + 6 x = 99; + 7 print(x,y); + +sources/0201_assign_cst2.c:2.0-11: [ x in [-oo;+oo], y in [-oo;+oo] ] +sources/0201_assign_cst2.c:4.0-11: [ x in [12;12], y in [-oo;+oo] ] +sources/0201_assign_cst2.c:7.0-11: [ x in [99;99], y in [15;15] ] +Output: [ x in [99;99], y in [15;15] ] + +------------------------------------- + +sources/0202_assign_expr.c + + 1 int x; + 2 x = 2 + 2; + +Output: [ x in [4;4] ] + +------------------------------------- + +sources/0203_assign_expr2.c + + 1 int x,y; + 2 x = 12; + 3 y = 16; + 4 x = x + y + 2; + 5 print(x); + +sources/0203_assign_expr2.c:5.0-9: [ x in [30;30] ] +Output: [ x in [30;30], y in [16;16] ] + +------------------------------------- + +sources/0204_assign_rand.c + + 1 int x; + 2 x = rand(1,99); + 3 print(x); + +sources/0204_assign_rand.c:3.0-9: [ x in [1;99] ] +Output: [ x in [1;99] ] + +------------------------------------- + +sources/0205_assign_rand2.c + + 1 int x; + 2 x = rand(10,-5); + 3 print(x); + +sources/0205_assign_rand2.c:3.0-9: bottom +Output: bottom + +------------------------------------- + +sources/0206_assign_add.c + + 1 int x; + 2 x = 2 + 5; + +Output: [ x in [7;7] ] + +------------------------------------- + +sources/0207_assign_add2.c + + 1 int x; + 2 x = rand(1,5) + rand (10,10); + +Output: [ x in [11;15] ] + +------------------------------------- + +sources/0208_assign_add3.c + + 1 int x; + 2 x = x + 2; + +Output: [ x in [-oo;+oo] ] + +------------------------------------- + +sources/0209_assign_neg.c + + 1 int x; + 2 x = -9; + +Output: [ x in [-9;-9] ] + +------------------------------------- + +sources/0210_assign_neg2.c + + 1 int x; + 2 x = -rand(-1,10); + 3 + +Output: [ x in [-10;1] ] + +------------------------------------- + +sources/0211_assign_sub.c + + 1 int x; + 2 x = 999 - 1; + +Output: [ x in [998;998] ] + +------------------------------------- + +sources/0212_assign_sub2.c + + 1 int x; + 2 x = rand(1,10) - rand(2,3); + +Output: [ x in [-2;8] ] + +------------------------------------- + +sources/0213_assign_mul.c + + 1 int x; + 2 x = 5 * 8; + +Output: [ x in [40;40] ] + +------------------------------------- + +sources/0214_assign_mul2.c + + 1 int x; + 2 x = rand(1,3) * rand(2,9); + +Output: [ x in [2;27] ] + +------------------------------------- + +sources/0215_assign_mul3.c + + 1 int x; + 2 x = rand(-5,3) * rand(-1,10); + +Output: [ x in [-50;30] ] + +------------------------------------- + +sources/0216_assign_mul4.c + + 1 int x; + 2 x = x * 0; + +Output: [ x in [0;0] ] + +------------------------------------- + +sources/0217_assign_copy.c + + 1 int x; + 2 int y; + 3 x = 12; + 4 y = x; + 5 print(y); + +sources/0217_assign_copy.c:5.0-9: [ y in [12;12] ] +Output: [ x in [12;12], y in [12;12] ] + +------------------------------------- + +sources/0218_assign_rel.c + + 1 int x; + 2 int y; + 3 x = 15; + 4 y = x + 2; + 5 print(y); + +sources/0218_assign_rel.c:5.0-9: [ y in [17;17] ] +Output: [ x in [15;15], y in [17;17] ] + +------------------------------------- + +sources/0219_assign_rel2.c + + 1 int x = rand(1,5); + 2 int y = rand(2,10); + 3 int z = x + 2*y; + +Output: [ x in [1;5], y in [2;10], z in [5;25] ] + +------------------------------------- + +sources/0300_if_true.c + + 1 int x = 1; + 2 if (1 <= 2) x = 9; + +Output: [ x in [9;9] ] + +------------------------------------- + +sources/0301_if_false.c + + 1 int x = 1; + 2 if (1 >= 2) x = 9; + +Output: [ x in [1;1] ] + +------------------------------------- + +sources/0302_if_both.c + + 1 int x = 1; + 2 if (rand(0,1) == 0) x = 9; + +Output: [ x in [1;9] ] + +------------------------------------- + +sources/0303_if_else_true.c + + 1 int x = 1; + 2 if (1 <= 2) x = 5; else x = 10; + +Output: [ x in [5;5] ] + +------------------------------------- + +sources/0304_if_else_false.c + + 1 int x = 1; + 2 if (1 >= 2) x = 5; else x = 10; + +Output: [ x in [10;10] ] + +------------------------------------- + +sources/0305_if_else_both.c + + 1 int x = 1; + 2 if (rand(0,1) == 0) x = 5; else x = 10; + +Output: [ x in [5;10] ] + +------------------------------------- + +sources/0306_if_rel.c + + 1 int x,y; + 2 if (rand(0,1) == 0) { x = 1; y = 3; } + 3 else { x = 2; y = 1; } + +Output: [ x in [1;2], y in [1;3] ] + +------------------------------------- + +sources/0307_if_var.c + + 1 int x = rand(-10,20); + 2 if (x >= 0) { print(x); } + 3 else { print(x); } + +sources/0307_if_var.c:2.14-24: [ x in [0;20] ] +sources/0307_if_var.c:3.7-17: [ x in [-10;-1] ] +Output: [ x in [-10;20] ] + +------------------------------------- + +sources/0308_if_var2.c + + 1 int x = rand(-20,10); + 2 if (x < 2) x = -x; + +Output: [ x in [-1;20] ] + +------------------------------------- + +sources/0309_if_var_rel.c + + 1 int x = rand(-10,25); + 2 int y = rand(-15,20); + 3 if (x >= y) x = y; + +Output: [ x in [-15;20], y in [-15;20] ] + +------------------------------------- + +sources/0310_cmp_le.c + + 1 int x = rand(10,20); + 2 int y = rand(15,30); + 3 if (x <= y) print(x,y); + +sources/0310_cmp_le.c:3.11-23: [ x in [10;20], y in [15;30] ] +Output: [ x in [10;20], y in [15;30] ] + +------------------------------------- + +sources/0311_cmp_le2.c + + 1 int x = rand(10,20); + 2 int y = rand(8,17); + 3 if (x <= y) print(x,y); + +sources/0311_cmp_le2.c:3.11-23: [ x in [10;17], y in [10;17] ] +Output: [ x in [10;20], y in [8;17] ] + +------------------------------------- + +sources/0312_cmp_le3.c + + 1 int y = rand(10,20); + 2 int x = rand(30,55); + 3 if (x <= y) print(x); + +sources/0312_cmp_le3.c:3.11-21: bottom +Output: [ x in [30;55], y in [10;20] ] + +------------------------------------- + +sources/0313_cmp_lt.c + + 1 int x = rand(10,20); + 2 int y = rand(5,15); + 3 if (x < y) print(x,y); + +sources/0313_cmp_lt.c:3.10-22: [ x in [10;14], y in [11;15] ] +Output: [ x in [10;20], y in [5;15] ] + +------------------------------------- + +sources/0314_cmp_ge.c + + 1 int x = rand(10,20); + 2 int y = rand(15,30); + 3 if (x >= y) print(x,y); + +sources/0314_cmp_ge.c:3.11-23: [ x in [15;20], y in [15;20] ] +Output: [ x in [10;20], y in [15;30] ] + +------------------------------------- + +sources/0315_cmp_gt.c + + 1 int x = rand(10,20); + 2 int y = rand(15,30); + 3 if (x > y) print(x,y); + +sources/0315_cmp_gt.c:3.10-22: [ x in [16;20], y in [15;19] ] +Output: [ x in [10;20], y in [15;30] ] + +------------------------------------- + +sources/0316_cmp_eq.c + + 1 int x = rand(15,30); + 2 int y = rand(10,20); + 3 if (x == y) print(x,y); + +sources/0316_cmp_eq.c:3.11-23: [ x in [15;20], y in [15;20] ] +Output: [ x in [15;30], y in [10;20] ] + +------------------------------------- + +sources/0317_cmp_eq2.c + + 1 int x = rand(15,20); + 2 int y = rand(25,30); + 3 if (x == y) print(x,y); + +sources/0317_cmp_eq2.c:3.11-23: bottom +Output: [ x in [15;20], y in [25;30] ] + +------------------------------------- + +sources/0318_cmp_ne.c + + 1 int x = rand(10,15); + 2 int y = rand(10,15); + 3 if (x != y) print(x,y); + +sources/0318_cmp_ne.c:3.11-23: [ x in [10;15], y in [10;15] ] +Output: [ x in [10;15], y in [10;15] ] + +------------------------------------- + +sources/0319_cmp_ne.c + + 1 int x = rand(10,15); + 2 int y = 10; + 3 if (x != y) print(x,y); + +sources/0319_cmp_ne.c:3.11-23: [ x in [11;15], y in [10;10] ] +Output: [ x in [10;15], y in [10;10] ] + +------------------------------------- + +sources/0320_cmp_eq_ne.c + + 1 int x = rand(10,15); + 2 int y = 10; + 3 if (x == y) print(x,y); + 4 else print(x,y); + 5 + +sources/0320_cmp_eq_ne.c:3.11-4.0: [ x in [10;10], y in [10;10] ] +sources/0320_cmp_eq_ne.c:4.4-16: [ x in [11;15], y in [10;10] ] +Output: [ x in [10;15], y in [10;10] ] + +------------------------------------- + +sources/0321_cmp_rel.c + + 1 int x = rand(10,20); + 2 int y = x; + 3 if (x >= 15) { print(y); } + +sources/0321_cmp_rel.c:3.15-25: [ y in [10;20] ] +Output: [ x in [10;20], y in [10;20] ] + +------------------------------------- + +sources/0322_if_and.c + + 1 int x = rand(10,20); + 2 int y = rand(30,40); + 3 if (x>=15 && y>=35) { print(x,y); } + 4 else { print(x,y); } + +sources/0322_if_and.c:3.22-34: [ x in [15;20], y in [35;40] ] +sources/0322_if_and.c:4.7-19: [ x in [10;20], y in [30;40] ] +Output: [ x in [10;20], y in [30;40] ] + +------------------------------------- + +sources/0323_if_or.c + + 1 int x = rand(10,20); + 2 int y = rand(30,40); + 3 if (x>=15 || y>=35) { print(x,y); } + 4 else { print(x,y); } + +sources/0323_if_or.c:3.22-34: [ x in [10;20], y in [30;40] ] +sources/0323_if_or.c:4.7-19: [ x in [10;14], y in [30;34] ] +Output: [ x in [10;20], y in [30;40] ] + +------------------------------------- + +sources/0324_if_not.c + + 1 int x = rand(10,20); + 2 int y = rand(30,40); + 3 if (!(x>=15) || y>=35) { print(x,y); } + 4 else { print(x,y); } + +sources/0324_if_not.c:3.25-37: [ x in [10;20], y in [30;40] ] +sources/0324_if_not.c:4.7-19: [ x in [15;20], y in [30;34] ] +Output: [ x in [10;20], y in [30;40] ] + +------------------------------------- + +sources/0325_if_bool.c + + 1 int x = rand(10,20); + 2 int y = rand(10,20); + 3 if (x<=15 && y>=15 || x>=15 && y<=15) { print(x,y); } + 4 else { print(x,y); } + +sources/0325_if_bool.c:3.40-52: [ x in [10;20], y in [10;20] ] +sources/0325_if_bool.c:4.7-19: [ x in [10;20], y in [10;20] ] +Output: [ x in [10;20], y in [10;20] ] + +------------------------------------- + +sources/0400_assert_true.c + + 1 int x = 2; + 2 assert(x>=1); + +Output: [ x in [2;2] ] + +------------------------------------- + +sources/0401_assert_false.c + + 1 int x = 9; + 2 assert (x < 5); + +sources/0401_assert_false.c:2.0-15: ERROR: assertion failure +Output: bottom + +------------------------------------- + +sources/0402_assert_both.c + + 1 int x = rand (-5,10); + 2 assert(x >= 0); + 3 assert(x > 0); + 4 + +sources/0402_assert_both.c:2.0-15: ERROR: assertion failure +sources/0402_assert_both.c:3.0-14: ERROR: assertion failure +Output: [ x in [1;10] ] + +------------------------------------- + +sources/0403_assert_both2.c + + 1 int x = rand (-5,10); + 2 assert(x > 0); + 3 assert(x >= 0); + +sources/0403_assert_both2.c:2.0-14: ERROR: assertion failure +Output: [ x in [1;10] ] + +------------------------------------- + +sources/0404_assert_rel.c + + 1 int x,y; + 2 if (rand(0,1)==0) { x = 1; y = 1; } + 3 else { x = 3 ; y = 3; } + 4 assert(x==y); + +sources/0404_assert_rel.c:4.0-13: ERROR: assertion failure +Output: [ x in [1;3], y in [1;3] ] + +------------------------------------- + +sources/0500_loop_count.c + + 1 int x = 0; + 2 while (x < 100) { + 3 print(x); + 4 x = x + 1; + 5 } + +sources/0500_loop_count.c:3.2-4.2: [ x in [0;0] ] +sources/0500_loop_count.c:3.2-4.2: [ x in [1;1] ] +sources/0500_loop_count.c:3.2-4.2: [ x in [2;2] ] +sources/0500_loop_count.c:3.2-4.2: [ x in [3;99] ] +Output: [ x in [100;100] ] + +------------------------------------- + +sources/0501_loop_infinite.c + + 1 int x = 0; + 2 while (x < 10) { + 3 print(x); + 4 } + +sources/0501_loop_infinite.c:3.2-4.0: [ x in [0;0] ] +sources/0501_loop_infinite.c:3.2-4.0: [ x in [0;0] ] +sources/0501_loop_infinite.c:3.2-4.0: [ x in [0;0] ] +sources/0501_loop_infinite.c:3.2-4.0: [ x in [0;0] ] +Output: bottom + +------------------------------------- + +sources/0502_loop_infinite2.c + + 1 int x = 0; + 2 while (x < 100) { + 3 print(x); + 4 x = x - 1; + 5 } + +sources/0502_loop_infinite2.c:3.2-4.2: [ x in [0;0] ] +sources/0502_loop_infinite2.c:3.2-4.2: [ x in [-1;-1] ] +sources/0502_loop_infinite2.c:3.2-4.2: [ x in [-2;-2] ] +sources/0502_loop_infinite2.c:3.2-4.2: [ x in [-oo;-3] ] +Output: bottom + +------------------------------------- + +sources/0503_loop_nondet.c + + 1 int x = 0; + 2 while (rand(0,1) == 0) { + 3 print(x); + 4 x = x + 1; + 5 } + +sources/0503_loop_nondet.c:3.2-4.2: [ x in [0;0] ] +sources/0503_loop_nondet.c:3.2-4.2: [ x in [1;1] ] +sources/0503_loop_nondet.c:3.2-4.2: [ x in [2;2] ] +sources/0503_loop_nondet.c:3.2-4.2: [ x in [3;+oo] ] +Output: [ x in [0;+oo] ] + +------------------------------------- + +sources/0504_loop_rel.c + + 1 int N = rand(0,1000); + 2 int x = 0; + 3 while (x < N) { + 4 print(x,N); + 5 x = x + 1; + 6 } + 7 assert(x==N); + +sources/0504_loop_rel.c:4.2-5.2: [ x in [0;0], N in [1;1000] ] +sources/0504_loop_rel.c:4.2-5.2: [ x in [1;1], N in [2;1000] ] +sources/0504_loop_rel.c:4.2-5.2: [ x in [2;2], N in [3;1000] ] +sources/0504_loop_rel.c:4.2-5.2: [ x in [3;999], N in [4;1000] ] +sources/0504_loop_rel.c:7.0-13: ERROR: assertion failure +Output: [ N in [0;1000], x in [0;1000] ] + +------------------------------------- + +sources/0505_loop_rel2.c + + 1 int N = rand(0,1000); + 2 int x = 0; + 3 while (x < N) { + 4 print(x,N); + 5 x = x + rand(0,3); + 6 } + 7 assert(x>=N && x<N+3); + +sources/0505_loop_rel2.c:4.2-5.2: [ x in [0;0], N in [1;1000] ] +sources/0505_loop_rel2.c:4.2-5.2: [ x in [0;3], N in [1;1000] ] +sources/0505_loop_rel2.c:4.2-5.2: [ x in [0;6], N in [1;1000] ] +sources/0505_loop_rel2.c:4.2-5.2: [ x in [0;999], N in [1;1000] ] +sources/0505_loop_rel2.c:7.0-22: ERROR: assertion failure +Output: [ N in [0;1000], x in [0;1002] ] + +------------------------------------- + +sources/0506_loop_limit.c + + 1 int x = 0; + 2 while (rand(0,1)==0) { + 3 if (x < 10000) x = x + 1; + 4 } + 5 print(x); + +sources/0506_loop_limit.c:5.0-9: [ x in [0;+oo] ] +Output: [ x in [0;+oo] ] + +------------------------------------- + +sources/0507_loop_limit2.c + + 1 int x = 0; + 2 int N = rand(0,1000); + 3 while (rand(0,1)==0) { + 4 if (x < N) x = x + 1; + 5 } + 6 print(x); + +sources/0507_loop_limit2.c:6.0-9: [ x in [0;+oo] ] +Output: [ N in [0;1000], x in [0;+oo] ] + +------------------------------------- + +sources/0508_loop_init.c + + 1 int init; + 2 int x; + 3 + 4 init = 0; + 5 while (rand(0,1)==0) { + 6 if (init == 0) { + 7 x = 0; + 8 init = 1; + 9 } +10 else { +11 x = x + 1; +12 } +13 assert(x >= 0); +14 } + +Output: [ init in [0;1], x in [-oo;+oo] ] + +------------------------------------- + +sources/0509_loop_nested.c + + 1 int i=0, j=0; + 2 + 3 while (i < 1000) { + 4 j = 0; + 5 while (j < i) { + 6 j = j + 1; + 7 } + 8 i = i + 1; + 9 } + +Output: [ i in [1000;1000], j in [2;999] ] + +------------------------------------- + +sources/0510_loop_nested2.c + + 1 int i,j; + 2 + 3 i = 0; + 4 while (i < 1000) { + 5 j = 0; + 6 while (j < i) { + 7 j = j + 1; + 8 } + 9 i = i + 1; +10 } + +Output: [ i in [1000;1000], j in [2;999] ] + +------------------------------------- + +sources/0600_bubble_sort.c + + 1 // Example from Cousot Habwachs POPL 1978 + 2 + 3 // Bubble sort, where array operations are abstracted away + 4 // to get a non-deterministic scalar program + 5 + 6 // expected results: + 7 // - with polyhedra, no assertion failure (proof of absence of array overflow) + 8 // - with intervals, assertion failure + 9 +10 int B,J,T; +11 int N = rand(0,100000); // array size +12 +13 B = N; +14 while (B >= 1) { +15 J = 1; +16 T = 0; +17 while (J <= B-1) { +18 +19 // array bound-check +20 assert(1 <= J && J <= N); +21 assert(1 <= (J+1) && (J+1) <= N); +22 +23 // the non-deterministic test models comparing TAB[J] and TAB[J+1] +24 if (rand(0,1)==0) { +25 // where, we would exchange TAB[J] and TAB[J+1]; +26 T = J; +27 } +28 +29 J = J + 1; +30 } +31 B = T; +32 } + +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +sources/0600_bubble_sort.c:20.4-21.4: ERROR: assertion failure +sources/0600_bubble_sort.c:21.4-24.4: ERROR: assertion failure +Output: [ B in [0;0], J in [-oo;+oo], N in [0;100000], T in [-oo;+oo] ] + +------------------------------------- + +sources/0601_heap_sort.c + + 1 // Example from Cousot Habwachs POPL 1978 + 2 + 3 // Heap sort, where array operations are abstracted away + 4 // to get a non-deterministic scalar program + 5 + 6 // expected results: with polyhedra, no assertion failure + 7 + 8 int L,R,I,J; + 9 int N = rand(1,100000); // array size +10 +11 L = N/2 + 1; +12 R = N; +13 +14 if (L >= 2) { +15 L = L - 1; +16 // model the assignment "K = TAB[L]" +17 assert(1 <= L && L <= N); +18 } +19 else { +20 // model the assignments "K = TAB[R]; TAB[R] = TAB[1]" +21 assert(1 <= R && R <= N); +22 assert(1 <= 1 && 1 <= N); +23 R = R - 1; +24 } +25 +26 while (R >= 2) { +27 I = L; +28 J = 2*I; +29 +30 while (J <= R && rand(0,1)==0) { +31 if (J <= R-1) { +32 // model the comparison "TAB[J] < TAB[J+1]" +33 assert(1 <= J && J <= N); +34 assert(1 <= (J+1) && (J+1) <= N); +35 if (rand(0,1)==0) { J = J + 1; } +36 } +37 +38 // model the comparison "K < TAB[J]" +39 assert(1 <= J && J <= N); +40 if (rand(0,1)==0) { +41 // model the assignment "TAB[I] = TAB[J]" +42 assert(1 <= I && I <= N); +43 assert(1 <= J && J <= N); +44 I = J; +45 J = 2*J; +46 } +47 } +48 +49 // model the assignment "TAB[I] = K" +50 assert(1 <= I && I <= N); +51 +52 if (L >= 2) { +53 L = L - 1; +54 // model the assignment "K = TAB[L]" +55 assert(1 <= L && L <= N); +56 } +57 else { +58 // model the assignments "K = TAB[R]; TAB[R] = TAB[1]" +59 assert(1 <= R && R <= N); +60 assert(1 <= 1 && 1 <= N); +61 R = R - 1; +62 } +63 +64 // model the assignment "TAB[1] = K" +65 assert(1 <= 1 && 1 <= N); +66 } + +sources/0601_heap_sort.c:17.2-18.0: ERROR: assertion failure +sources/0601_heap_sort.c:21.3-22.3: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:33.6-34.6: ERROR: assertion failure +sources/0601_heap_sort.c:34.6-35.6: ERROR: assertion failure +sources/0601_heap_sort.c:39.4-40.4: ERROR: assertion failure +sources/0601_heap_sort.c:42.6-43.6: ERROR: assertion failure +sources/0601_heap_sort.c:43.6-44.6: ERROR: assertion failure +sources/0601_heap_sort.c:50.2-52.2: ERROR: assertion failure +sources/0601_heap_sort.c:55.4-56.2: ERROR: assertion failure +sources/0601_heap_sort.c:59.4-60.4: ERROR: assertion failure +Output: [ I in [-oo;+oo], J in [-oo;+oo], L in [-oo;100000], N in [1;100000], R in [0;1] ] + +------------------------------------- + +sources/0602_rate_limiter.c + + 1 // Example from Miné HOSC 2006 + 2 + 3 // Rate limiter: at each loop iteration, a new input is fetched (X) and + 4 // a new output (Y) is computed; Y tries to follow X but is limited to + 5 // change no more that a given slope (D) in absolute value + 6 + 7 // To prove that the assertion holds, this version needs the polyhedra + 8 // domain and an unrolling factor of at least 6 + 9 +10 int X; // input +11 int Y; // output +12 int S; // last output +13 int D; // maximum slope; +14 +15 Y = 0; +16 while (rand(0,1)==1) { +17 X = rand(-128,128); +18 D = rand(0,16); +19 S = Y; +20 int R = X - S; // current slope +21 Y = X; +22 if (R <= -D) Y = S - D; // slope too small +23 else if (R >= D) Y = S + D; // slope too large +24 } +25 +26 assert(Y >= -128 && Y <= 128); + +sources/0602_rate_limiter.c:26.0-30: ERROR: assertion failure +Output: [ D in [-oo;+oo], S in [-oo;+oo], X in [-oo;+oo], Y in [-128;128] ] + +------------------------------------- + +sources/0603_rate_limiter2.c + + 1 // This version is similar to the previous one, but the assertion is checked + 2 // inside the loop + 3 // No unrolling is necessary in this version! + 4 + 5 int X; // input + 6 int Y; // output + 7 int S; // last output + 8 int D; // maximum slope; + 9 +10 Y = 0; +11 while (rand(0,1)==1) { +12 X = rand(-128,128); +13 D = rand(0,16); +14 S = Y; +15 int R = X - S; // current slope +16 Y = X; +17 if (R <= -D) Y = S - D; // slope too small +18 else if (R >= D) Y = S + D; // slope too large +19 +20 assert(Y >= -128 && Y <= 128); +21 } + +sources/0603_rate_limiter2.c:20.2-21.0: ERROR: assertion failure +sources/0603_rate_limiter2.c:20.2-21.0: ERROR: assertion failure +sources/0603_rate_limiter2.c:20.2-21.0: ERROR: assertion failure +Output: [ D in [-oo;+oo], S in [-oo;+oo], X in [-oo;+oo], Y in [-128;128] ] + +------------------------------------- + diff --git a/tests/results/all.polyhedra.txt b/tests/results/all.polyhedra.txt new file mode 100644 index 0000000..65a3b93 --- /dev/null +++ b/tests/results/all.polyhedra.txt @@ -0,0 +1,998 @@ +sources/0000_noinit_var.c + + 1 int x; + +Output: top + +------------------------------------- + +sources/0001_noinit_2var.c + + 1 int x; + 2 int y; + +Output: top + +------------------------------------- + +sources/0002_init_var.c + + 1 int x = 0; + +Output: [|x=0|] + +------------------------------------- + +sources/0003_init_2var.c + + 1 int x = 0; + 2 int y = 1; + +Output: [|y-1=0; x=0|] + +------------------------------------- + +sources/0004_init_2var2.c + + 1 int x = 9, y = 12; + +Output: [|y-12=0; x-9=0|] + +------------------------------------- + +sources/0100_print_var.c + + 1 int x = 2; + 2 print(x); + +sources/0100_print_var.c:2.0-9: [|x-2=0|] +Output: [|x-2=0|] + +------------------------------------- + +sources/0101_print_2var.c + + 1 int x = 3; + 2 int y = 15; + 3 print(y); + +sources/0101_print_2var.c:3.0-9: [|y-15=0|] +Output: [|y-15=0; x-3=0|] + +------------------------------------- + +sources/0102_print_3var.c + + 1 int x = 3; + 2 int y = 15; + 3 int z = 99; + 4 print(z,x); + +sources/0102_print_3var.c:4.0-11: [|z-99=0; x-3=0|] +Output: [|z-99=0; y-15=0; x-3=0|] + +------------------------------------- + +sources/0103_local.c + + 1 int x = 12; + 2 { + 3 int y = 9; + 4 print(x,y); + 5 } + +sources/0103_local.c:4.2-5.0: [|y-9=0; x-12=0|] +Output: [|x-12=0|] + +------------------------------------- + +sources/0200_assign_cst.c + + 1 int x; + 2 print(x); + 3 x = 12; + 4 print(x); + 5 x = 15; + 6 print(x); + +sources/0200_assign_cst.c:2.0-9: top +sources/0200_assign_cst.c:4.0-9: [|x-12=0|] +sources/0200_assign_cst.c:6.0-9: [|x-15=0|] +Output: [|x-15=0|] + +------------------------------------- + +sources/0201_assign_cst2.c + + 1 int x, y; + 2 print(x,y); + 3 x = 12; + 4 print(x,y); + 5 y = 15; + 6 x = 99; + 7 print(x,y); + +sources/0201_assign_cst2.c:2.0-11: top +sources/0201_assign_cst2.c:4.0-11: [|x-12=0|] +sources/0201_assign_cst2.c:7.0-11: [|y-15=0; x-99=0|] +Output: [|y-15=0; x-99=0|] + +------------------------------------- + +sources/0202_assign_expr.c + + 1 int x; + 2 x = 2 + 2; + +Output: [|x-4=0|] + +------------------------------------- + +sources/0203_assign_expr2.c + + 1 int x,y; + 2 x = 12; + 3 y = 16; + 4 x = x + y + 2; + 5 print(x); + +sources/0203_assign_expr2.c:5.0-9: [|x-30=0|] +Output: [|y-16=0; x-30=0|] + +------------------------------------- + +sources/0204_assign_rand.c + + 1 int x; + 2 x = rand(1,99); + 3 print(x); + +sources/0204_assign_rand.c:3.0-9: [|-x+99>=0; x-1>=0|] +Output: [|-x+99>=0; x-1>=0|] + +------------------------------------- + +sources/0205_assign_rand2.c + + 1 int x; + 2 x = rand(10,-5); + 3 print(x); + +sources/0205_assign_rand2.c:3.0-9: bottom +Output: bottom + +------------------------------------- + +sources/0206_assign_add.c + + 1 int x; + 2 x = 2 + 5; + +Output: [|x-7=0|] + +------------------------------------- + +sources/0207_assign_add2.c + + 1 int x; + 2 x = rand(1,5) + rand (10,10); + +Output: [|-x+15>=0; x-11>=0|] + +------------------------------------- + +sources/0208_assign_add3.c + + 1 int x; + 2 x = x + 2; + +Output: top + +------------------------------------- + +sources/0209_assign_neg.c + + 1 int x; + 2 x = -9; + +Output: [|x+9=0|] + +------------------------------------- + +sources/0210_assign_neg2.c + + 1 int x; + 2 x = -rand(-1,10); + 3 + +Output: [|-x+1>=0; x+10>=0|] + +------------------------------------- + +sources/0211_assign_sub.c + + 1 int x; + 2 x = 999 - 1; + +Output: [|x-998=0|] + +------------------------------------- + +sources/0212_assign_sub2.c + + 1 int x; + 2 x = rand(1,10) - rand(2,3); + +Output: [|-x+8>=0; x+2>=0|] + +------------------------------------- + +sources/0213_assign_mul.c + + 1 int x; + 2 x = 5 * 8; + +Output: [|x-40=0|] + +------------------------------------- + +sources/0214_assign_mul2.c + + 1 int x; + 2 x = rand(1,3) * rand(2,9); + +Output: [|-x+27>=0; x-2>=0|] + +------------------------------------- + +sources/0215_assign_mul3.c + + 1 int x; + 2 x = rand(-5,3) * rand(-1,10); + +Output: [|-x+30>=0; x+50>=0|] + +------------------------------------- + +sources/0216_assign_mul4.c + + 1 int x; + 2 x = x * 0; + +Output: [|x=0|] + +------------------------------------- + +sources/0217_assign_copy.c + + 1 int x; + 2 int y; + 3 x = 12; + 4 y = x; + 5 print(y); + +sources/0217_assign_copy.c:5.0-9: [|y-12=0|] +Output: [|y-12=0; x-12=0|] + +------------------------------------- + +sources/0218_assign_rel.c + + 1 int x; + 2 int y; + 3 x = 15; + 4 y = x + 2; + 5 print(y); + +sources/0218_assign_rel.c:5.0-9: [|y-17=0|] +Output: [|y-17=0; x-15=0|] + +------------------------------------- + +sources/0219_assign_rel2.c + + 1 int x = rand(1,5); + 2 int y = rand(2,10); + 3 int z = x + 2*y; + +Output: [|-x-2y+z=0; -x+5>=0; -y+10>=0; y-2>=0; x-1>=0|] + +------------------------------------- + +sources/0300_if_true.c + + 1 int x = 1; + 2 if (1 <= 2) x = 9; + +Output: [|x-9=0|] + +------------------------------------- + +sources/0301_if_false.c + + 1 int x = 1; + 2 if (1 >= 2) x = 9; + +Output: [|x-1=0|] + +------------------------------------- + +sources/0302_if_both.c + + 1 int x = 1; + 2 if (rand(0,1) == 0) x = 9; + +Output: [|-x+9>=0; x-1>=0|] + +------------------------------------- + +sources/0303_if_else_true.c + + 1 int x = 1; + 2 if (1 <= 2) x = 5; else x = 10; + +Output: [|x-5=0|] + +------------------------------------- + +sources/0304_if_else_false.c + + 1 int x = 1; + 2 if (1 >= 2) x = 5; else x = 10; + +Output: [|x-10=0|] + +------------------------------------- + +sources/0305_if_else_both.c + + 1 int x = 1; + 2 if (rand(0,1) == 0) x = 5; else x = 10; + +Output: [|-x+10>=0; x-5>=0|] + +------------------------------------- + +sources/0306_if_rel.c + + 1 int x,y; + 2 if (rand(0,1) == 0) { x = 1; y = 3; } + 3 else { x = 2; y = 1; } + +Output: [|2x+y-5=0; -x+2>=0; x-1>=0|] + +------------------------------------- + +sources/0307_if_var.c + + 1 int x = rand(-10,20); + 2 if (x >= 0) { print(x); } + 3 else { print(x); } + +sources/0307_if_var.c:2.14-24: [|-x+20>=0; x>=0|] +sources/0307_if_var.c:3.7-17: [|-x-1>=0; x+10>=0|] +Output: [|-x+20>=0; x+10>=0|] + +------------------------------------- + +sources/0308_if_var2.c + + 1 int x = rand(-20,10); + 2 if (x < 2) x = -x; + +Output: [|-x+20>=0; x+1>=0|] + +------------------------------------- + +sources/0309_if_var_rel.c + + 1 int x = rand(-10,25); + 2 int y = rand(-15,20); + 3 if (x >= y) x = y; + +Output: [|-x+y>=0; -y+20>=0; 7x-y+90>=0|] + +------------------------------------- + +sources/0310_cmp_le.c + + 1 int x = rand(10,20); + 2 int y = rand(15,30); + 3 if (x <= y) print(x,y); + +sources/0310_cmp_le.c:3.11-23: [|-x+20>=0; -x+y>=0; -y+30>=0; y-15>=0; + x-10>=0|] +Output: [|-x+20>=0; -y+30>=0; y-15>=0; x-10>=0|] + +------------------------------------- + +sources/0311_cmp_le2.c + + 1 int x = rand(10,20); + 2 int y = rand(8,17); + 3 if (x <= y) print(x,y); + +sources/0311_cmp_le2.c:3.11-23: [|-x+y>=0; -y+17>=0; x-10>=0|] +Output: [|-x+20>=0; -y+17>=0; y-8>=0; x-10>=0|] + +------------------------------------- + +sources/0312_cmp_le3.c + + 1 int y = rand(10,20); + 2 int x = rand(30,55); + 3 if (x <= y) print(x); + +sources/0312_cmp_le3.c:3.11-21: bottom +Output: [|-x+55>=0; -y+20>=0; y-10>=0; x-30>=0|] + +------------------------------------- + +sources/0313_cmp_lt.c + + 1 int x = rand(10,20); + 2 int y = rand(5,15); + 3 if (x < y) print(x,y); + +sources/0313_cmp_lt.c:3.10-22: [|-x+y-1>=0; -y+15>=0; x-10>=0|] +Output: [|-x+20>=0; -y+15>=0; y-5>=0; x-10>=0|] + +------------------------------------- + +sources/0314_cmp_ge.c + + 1 int x = rand(10,20); + 2 int y = rand(15,30); + 3 if (x >= y) print(x,y); + +sources/0314_cmp_ge.c:3.11-23: [|-x+20>=0; y-15>=0; x-y>=0|] +Output: [|-x+20>=0; -y+30>=0; y-15>=0; x-10>=0|] + +------------------------------------- + +sources/0315_cmp_gt.c + + 1 int x = rand(10,20); + 2 int y = rand(15,30); + 3 if (x > y) print(x,y); + +sources/0315_cmp_gt.c:3.10-22: [|-x+20>=0; y-15>=0; x-y-1>=0|] +Output: [|-x+20>=0; -y+30>=0; y-15>=0; x-10>=0|] + +------------------------------------- + +sources/0316_cmp_eq.c + + 1 int x = rand(15,30); + 2 int y = rand(10,20); + 3 if (x == y) print(x,y); + +sources/0316_cmp_eq.c:3.11-23: [|-x+y=0; -x+20>=0; x-15>=0|] +Output: [|-x+30>=0; -y+20>=0; y-10>=0; x-15>=0|] + +------------------------------------- + +sources/0317_cmp_eq2.c + + 1 int x = rand(15,20); + 2 int y = rand(25,30); + 3 if (x == y) print(x,y); + +sources/0317_cmp_eq2.c:3.11-23: bottom +Output: [|-x+20>=0; -y+30>=0; y-25>=0; x-15>=0|] + +------------------------------------- + +sources/0318_cmp_ne.c + + 1 int x = rand(10,15); + 2 int y = rand(10,15); + 3 if (x != y) print(x,y); + +sources/0318_cmp_ne.c:3.11-23: [|-x-y+29>=0; -x+15>=0; -y+15>=0; y-10>=0; + x-10>=0; x+y-21>=0|] +Output: [|-x+15>=0; -y+15>=0; y-10>=0; x-10>=0|] + +------------------------------------- + +sources/0319_cmp_ne.c + + 1 int x = rand(10,15); + 2 int y = 10; + 3 if (x != y) print(x,y); + +sources/0319_cmp_ne.c:3.11-23: [|y-10=0; -x+15>=0; x-11>=0|] +Output: [|y-10=0; -x+15>=0; x-10>=0|] + +------------------------------------- + +sources/0320_cmp_eq_ne.c + + 1 int x = rand(10,15); + 2 int y = 10; + 3 if (x == y) print(x,y); + 4 else print(x,y); + 5 + +sources/0320_cmp_eq_ne.c:3.11-4.0: [|y-10=0; x-10=0|] +sources/0320_cmp_eq_ne.c:4.4-16: [|y-10=0; -x+15>=0; x-11>=0|] +Output: [|y-10=0; -x+15>=0; x-10>=0|] + +------------------------------------- + +sources/0321_cmp_rel.c + + 1 int x = rand(10,20); + 2 int y = x; + 3 if (x >= 15) { print(y); } + +sources/0321_cmp_rel.c:3.15-25: [|-y+20>=0; y-15>=0|] +Output: [|-x+y=0; -x+20>=0; x-10>=0|] + +------------------------------------- + +sources/0322_if_and.c + + 1 int x = rand(10,20); + 2 int y = rand(30,40); + 3 if (x>=15 && y>=35) { print(x,y); } + 4 else { print(x,y); } + +sources/0322_if_and.c:3.22-34: [|-x+20>=0; -y+40>=0; y-35>=0; x-15>=0|] +sources/0322_if_and.c:4.7-19: [|-x-y+54>=0; -x+20>=0; -y+40>=0; y-30>=0; + x-10>=0|] +Output: [|-x+20>=0; -y+40>=0; y-30>=0; x-10>=0|] + +------------------------------------- + +sources/0323_if_or.c + + 1 int x = rand(10,20); + 2 int y = rand(30,40); + 3 if (x>=15 || y>=35) { print(x,y); } + 4 else { print(x,y); } + +sources/0323_if_or.c:3.22-34: [|-x+20>=0; -y+40>=0; y-30>=0; x-10>=0; + x+y-45>=0|] +sources/0323_if_or.c:4.7-19: [|-x+14>=0; -y+34>=0; y-30>=0; x-10>=0|] +Output: [|-x+20>=0; -y+40>=0; y-30>=0; x-10>=0|] + +------------------------------------- + +sources/0324_if_not.c + + 1 int x = rand(10,20); + 2 int y = rand(30,40); + 3 if (!(x>=15) || y>=35) { print(x,y); } + 4 else { print(x,y); } + +sources/0324_if_not.c:3.25-37: [|-5x+6y-110>=0; -x+20>=0; -y+40>=0; y-30>=0; + x-10>=0|] +sources/0324_if_not.c:4.7-19: [|-x+20>=0; -y+34>=0; y-30>=0; x-15>=0|] +Output: [|-x+20>=0; -y+40>=0; y-30>=0; x-10>=0|] + +------------------------------------- + +sources/0325_if_bool.c + + 1 int x = rand(10,20); + 2 int y = rand(10,20); + 3 if (x<=15 && y>=15 || x>=15 && y<=15) { print(x,y); } + 4 else { print(x,y); } + +sources/0325_if_bool.c:3.40-52: [|-x-y+35>=0; -x+20>=0; -y+20>=0; y-10>=0; + x-10>=0; x+y-25>=0|] +sources/0325_if_bool.c:4.7-19: [|-x+20>=0; -x+y+4>=0; -y+20>=0; y-10>=0; + x-y+4>=0; x-10>=0|] +Output: [|-x+20>=0; -y+20>=0; y-10>=0; x-10>=0|] + +------------------------------------- + +sources/0400_assert_true.c + + 1 int x = 2; + 2 assert(x>=1); + +Output: [|x-2=0|] + +------------------------------------- + +sources/0401_assert_false.c + + 1 int x = 9; + 2 assert (x < 5); + +sources/0401_assert_false.c:2.0-15: ERROR: assertion failure +Output: bottom + +------------------------------------- + +sources/0402_assert_both.c + + 1 int x = rand (-5,10); + 2 assert(x >= 0); + 3 assert(x > 0); + 4 + +sources/0402_assert_both.c:2.0-15: ERROR: assertion failure +sources/0402_assert_both.c:3.0-14: ERROR: assertion failure +Output: [|-x+10>=0; x-1>=0|] + +------------------------------------- + +sources/0403_assert_both2.c + + 1 int x = rand (-5,10); + 2 assert(x > 0); + 3 assert(x >= 0); + +sources/0403_assert_both2.c:2.0-14: ERROR: assertion failure +Output: [|-x+10>=0; x-1>=0|] + +------------------------------------- + +sources/0404_assert_rel.c + + 1 int x,y; + 2 if (rand(0,1)==0) { x = 1; y = 1; } + 3 else { x = 3 ; y = 3; } + 4 assert(x==y); + +Output: [|-x+y=0; -x+3>=0; x-1>=0|] + +------------------------------------- + +sources/0500_loop_count.c + + 1 int x = 0; + 2 while (x < 100) { + 3 print(x); + 4 x = x + 1; + 5 } + +sources/0500_loop_count.c:3.2-4.2: [|x=0|] +sources/0500_loop_count.c:3.2-4.2: [|x-1=0|] +sources/0500_loop_count.c:3.2-4.2: [|x-2=0|] +sources/0500_loop_count.c:3.2-4.2: [|-x+99>=0; x-3>=0|] +Output: [|x-100=0|] + +------------------------------------- + +sources/0501_loop_infinite.c + + 1 int x = 0; + 2 while (x < 10) { + 3 print(x); + 4 } + +sources/0501_loop_infinite.c:3.2-4.0: [|x=0|] +sources/0501_loop_infinite.c:3.2-4.0: [|x=0|] +sources/0501_loop_infinite.c:3.2-4.0: [|x=0|] +sources/0501_loop_infinite.c:3.2-4.0: [|x=0|] +Output: bottom + +------------------------------------- + +sources/0502_loop_infinite2.c + + 1 int x = 0; + 2 while (x < 100) { + 3 print(x); + 4 x = x - 1; + 5 } + +sources/0502_loop_infinite2.c:3.2-4.2: [|x=0|] +sources/0502_loop_infinite2.c:3.2-4.2: [|x+1=0|] +sources/0502_loop_infinite2.c:3.2-4.2: [|x+2=0|] +sources/0502_loop_infinite2.c:3.2-4.2: [|-x-3>=0|] +Output: bottom + +------------------------------------- + +sources/0503_loop_nondet.c + + 1 int x = 0; + 2 while (rand(0,1) == 0) { + 3 print(x); + 4 x = x + 1; + 5 } + +sources/0503_loop_nondet.c:3.2-4.2: [|x=0|] +sources/0503_loop_nondet.c:3.2-4.2: [|x-1=0|] +sources/0503_loop_nondet.c:3.2-4.2: [|x-2=0|] +sources/0503_loop_nondet.c:3.2-4.2: [|x-3>=0|] +Output: [|x>=0|] + +------------------------------------- + +sources/0504_loop_rel.c + + 1 int N = rand(0,1000); + 2 int x = 0; + 3 while (x < N) { + 4 print(x,N); + 5 x = x + 1; + 6 } + 7 assert(x==N); + +sources/0504_loop_rel.c:4.2-5.2: [|x=0; -N+1000>=0; N-1>=0|] +sources/0504_loop_rel.c:4.2-5.2: [|x-1=0; -N+1000>=0; N-2>=0|] +sources/0504_loop_rel.c:4.2-5.2: [|x-2=0; -N+1000>=0; N-3>=0|] +sources/0504_loop_rel.c:4.2-5.2: [|-N+1000>=0; x-3>=0; N-x-1>=0|] +Output: [|-N+x=0; -N+1000>=0; N>=0|] + +------------------------------------- + +sources/0505_loop_rel2.c + + 1 int N = rand(0,1000); + 2 int x = 0; + 3 while (x < N) { + 4 print(x,N); + 5 x = x + rand(0,3); + 6 } + 7 assert(x>=N && x<N+3); + +sources/0505_loop_rel2.c:4.2-5.2: [|x=0; -N+1000>=0; N-1>=0|] +sources/0505_loop_rel2.c:4.2-5.2: [|-N+1000>=0; -x+3>=0; x>=0; N-x-1>=0|] +sources/0505_loop_rel2.c:4.2-5.2: [|-N+1000>=0; -x+6>=0; x>=0; N-x-1>=0|] +sources/0505_loop_rel2.c:4.2-5.2: [|-N+1000>=0; x>=0; N-x-1>=0|] +Output: [|-N+1000>=0; -N+x>=0; N-x+2>=0; 3N-x>=0|] + +------------------------------------- + +sources/0506_loop_limit.c + + 1 int x = 0; + 2 while (rand(0,1)==0) { + 3 if (x < 10000) x = x + 1; + 4 } + 5 print(x); + +sources/0506_loop_limit.c:5.0-9: [|x>=0|] +Output: [|x>=0|] + +------------------------------------- + +sources/0507_loop_limit2.c + + 1 int x = 0; + 2 int N = rand(0,1000); + 3 while (rand(0,1)==0) { + 4 if (x < N) x = x + 1; + 5 } + 6 print(x); + +sources/0507_loop_limit2.c:6.0-9: [|-x+1000>=0; x>=0|] +Output: [|-N+1000>=0; x>=0; N-x>=0|] + +------------------------------------- + +sources/0508_loop_init.c + + 1 int init; + 2 int x; + 3 + 4 init = 0; + 5 while (rand(0,1)==0) { + 6 if (init == 0) { + 7 x = 0; + 8 init = 1; + 9 } +10 else { +11 x = x + 1; +12 } +13 assert(x >= 0); +14 } + +Output: [|-init+1>=0; init>=0|] + +------------------------------------- + +sources/0509_loop_nested.c + + 1 int i=0, j=0; + 2 + 3 while (i < 1000) { + 4 j = 0; + 5 while (j < i) { + 6 j = j + 1; + 7 } + 8 i = i + 1; + 9 } + +Output: [|j-999=0; i-1000=0|] + +------------------------------------- + +sources/0510_loop_nested2.c + + 1 int i,j; + 2 + 3 i = 0; + 4 while (i < 1000) { + 5 j = 0; + 6 while (j < i) { + 7 j = j + 1; + 8 } + 9 i = i + 1; +10 } + +Output: [|j-999=0; i-1000=0|] + +------------------------------------- + +sources/0600_bubble_sort.c + + 1 // Example from Cousot Habwachs POPL 1978 + 2 + 3 // Bubble sort, where array operations are abstracted away + 4 // to get a non-deterministic scalar program + 5 + 6 // expected results: + 7 // - with polyhedra, no assertion failure (proof of absence of array overflow) + 8 // - with intervals, assertion failure + 9 +10 int B,J,T; +11 int N = rand(0,100000); // array size +12 +13 B = N; +14 while (B >= 1) { +15 J = 1; +16 T = 0; +17 while (J <= B-1) { +18 +19 // array bound-check +20 assert(1 <= J && J <= N); +21 assert(1 <= (J+1) && (J+1) <= N); +22 +23 // the non-deterministic test models comparing TAB[J] and TAB[J+1] +24 if (rand(0,1)==0) { +25 // where, we would exchange TAB[J] and TAB[J+1]; +26 T = J; +27 } +28 +29 J = J + 1; +30 } +31 B = T; +32 } + +Output: [|B=0; -N+100000>=0; N>=0|] + +------------------------------------- + +sources/0601_heap_sort.c + + 1 // Example from Cousot Habwachs POPL 1978 + 2 + 3 // Heap sort, where array operations are abstracted away + 4 // to get a non-deterministic scalar program + 5 + 6 // expected results: with polyhedra, no assertion failure + 7 + 8 int L,R,I,J; + 9 int N = rand(1,100000); // array size +10 +11 L = N/2 + 1; +12 R = N; +13 +14 if (L >= 2) { +15 L = L - 1; +16 // model the assignment "K = TAB[L]" +17 assert(1 <= L && L <= N); +18 } +19 else { +20 // model the assignments "K = TAB[R]; TAB[R] = TAB[1]" +21 assert(1 <= R && R <= N); +22 assert(1 <= 1 && 1 <= N); +23 R = R - 1; +24 } +25 +26 while (R >= 2) { +27 I = L; +28 J = 2*I; +29 +30 while (J <= R && rand(0,1)==0) { +31 if (J <= R-1) { +32 // model the comparison "TAB[J] < TAB[J+1]" +33 assert(1 <= J && J <= N); +34 assert(1 <= (J+1) && (J+1) <= N); +35 if (rand(0,1)==0) { J = J + 1; } +36 } +37 +38 // model the comparison "K < TAB[J]" +39 assert(1 <= J && J <= N); +40 if (rand(0,1)==0) { +41 // model the assignment "TAB[I] = TAB[J]" +42 assert(1 <= I && I <= N); +43 assert(1 <= J && J <= N); +44 I = J; +45 J = 2*J; +46 } +47 } +48 +49 // model the assignment "TAB[I] = K" +50 assert(1 <= I && I <= N); +51 +52 if (L >= 2) { +53 L = L - 1; +54 // model the assignment "K = TAB[L]" +55 assert(1 <= L && L <= N); +56 } +57 else { +58 // model the assignments "K = TAB[R]; TAB[R] = TAB[1]" +59 assert(1 <= R && R <= N); +60 assert(1 <= 1 && 1 <= N); +61 R = R - 1; +62 } +63 +64 // model the assignment "TAB[1] = K" +65 assert(1 <= 1 && 1 <= N); +66 } + +Output: [|-99999L+49999R+99999>=0; -2L+N+1>=0; -R+1>=0; L-1>=0|] + +------------------------------------- + +sources/0602_rate_limiter.c + + 1 // Example from Miné HOSC 2006 + 2 + 3 // Rate limiter: at each loop iteration, a new input is fetched (X) and + 4 // a new output (Y) is computed; Y tries to follow X but is limited to + 5 // change no more that a given slope (D) in absolute value + 6 + 7 // To prove that the assertion holds, this version needs the polyhedra + 8 // domain and an unrolling factor of at least 6 + 9 +10 int X; // input +11 int Y; // output +12 int S; // last output +13 int D; // maximum slope; +14 +15 Y = 0; +16 while (rand(0,1)==1) { +17 X = rand(-128,128); +18 D = rand(0,16); +19 S = Y; +20 int R = X - S; // current slope +21 Y = X; +22 if (R <= -D) Y = S - D; // slope too small +23 else if (R >= D) Y = S + D; // slope too large +24 } +25 +26 assert(Y >= -128 && Y <= 128); + +sources/0602_rate_limiter.c:26.0-30: ERROR: assertion failure +Output: [|-Y+128>=0; Y+128>=0|] + +------------------------------------- + +sources/0603_rate_limiter2.c + + 1 // This version is similar to the previous one, but the assertion is checked + 2 // inside the loop + 3 // No unrolling is necessary in this version! + 4 + 5 int X; // input + 6 int Y; // output + 7 int S; // last output + 8 int D; // maximum slope; + 9 +10 Y = 0; +11 while (rand(0,1)==1) { +12 X = rand(-128,128); +13 D = rand(0,16); +14 S = Y; +15 int R = X - S; // current slope +16 Y = X; +17 if (R <= -D) Y = S - D; // slope too small +18 else if (R >= D) Y = S + D; // slope too large +19 +20 assert(Y >= -128 && Y <= 128); +21 } + +Output: [|-Y+128>=0; Y+128>=0|] + +------------------------------------- + diff --git a/tests/sources/0000_noinit_var.c b/tests/sources/0000_noinit_var.c new file mode 100644 index 0000000..6d1a0d4 --- /dev/null +++ b/tests/sources/0000_noinit_var.c @@ -0,0 +1 @@ +int x; diff --git a/tests/sources/0001_noinit_2var.c b/tests/sources/0001_noinit_2var.c new file mode 100644 index 0000000..2b9d16b --- /dev/null +++ b/tests/sources/0001_noinit_2var.c @@ -0,0 +1,2 @@ +int x; +int y; diff --git a/tests/sources/0002_init_var.c b/tests/sources/0002_init_var.c new file mode 100644 index 0000000..15bfa8f --- /dev/null +++ b/tests/sources/0002_init_var.c @@ -0,0 +1 @@ +int x = 0; diff --git a/tests/sources/0003_init_2var.c b/tests/sources/0003_init_2var.c new file mode 100644 index 0000000..83aefaf --- /dev/null +++ b/tests/sources/0003_init_2var.c @@ -0,0 +1,2 @@ +int x = 0; +int y = 1; diff --git a/tests/sources/0004_init_2var2.c b/tests/sources/0004_init_2var2.c new file mode 100644 index 0000000..f81c09c --- /dev/null +++ b/tests/sources/0004_init_2var2.c @@ -0,0 +1 @@ +int x = 9, y = 12; diff --git a/tests/sources/0100_print_var.c b/tests/sources/0100_print_var.c new file mode 100644 index 0000000..e2f9464 --- /dev/null +++ b/tests/sources/0100_print_var.c @@ -0,0 +1,2 @@ +int x = 2; +print(x); diff --git a/tests/sources/0101_print_2var.c b/tests/sources/0101_print_2var.c new file mode 100644 index 0000000..92aa4a9 --- /dev/null +++ b/tests/sources/0101_print_2var.c @@ -0,0 +1,3 @@ +int x = 3; +int y = 15; +print(y); diff --git a/tests/sources/0102_print_3var.c b/tests/sources/0102_print_3var.c new file mode 100644 index 0000000..81fe534 --- /dev/null +++ b/tests/sources/0102_print_3var.c @@ -0,0 +1,4 @@ +int x = 3; +int y = 15; +int z = 99; +print(z,x); diff --git a/tests/sources/0103_local.c b/tests/sources/0103_local.c new file mode 100644 index 0000000..c6683be --- /dev/null +++ b/tests/sources/0103_local.c @@ -0,0 +1,5 @@ +int x = 12; +{ + int y = 9; + print(x,y); +} diff --git a/tests/sources/0200_assign_cst.c b/tests/sources/0200_assign_cst.c new file mode 100644 index 0000000..8340469 --- /dev/null +++ b/tests/sources/0200_assign_cst.c @@ -0,0 +1,6 @@ +int x; +print(x); +x = 12; +print(x); +x = 15; +print(x); diff --git a/tests/sources/0201_assign_cst2.c b/tests/sources/0201_assign_cst2.c new file mode 100644 index 0000000..6f28061 --- /dev/null +++ b/tests/sources/0201_assign_cst2.c @@ -0,0 +1,7 @@ +int x, y; +print(x,y); +x = 12; +print(x,y); +y = 15; +x = 99; +print(x,y); diff --git a/tests/sources/0202_assign_expr.c b/tests/sources/0202_assign_expr.c new file mode 100644 index 0000000..7d16636 --- /dev/null +++ b/tests/sources/0202_assign_expr.c @@ -0,0 +1,2 @@ +int x; +x = 2 + 2; diff --git a/tests/sources/0203_assign_expr2.c b/tests/sources/0203_assign_expr2.c new file mode 100644 index 0000000..7583362 --- /dev/null +++ b/tests/sources/0203_assign_expr2.c @@ -0,0 +1,5 @@ +int x,y; +x = 12; +y = 16; +x = x + y + 2; +print(x); diff --git a/tests/sources/0204_assign_rand.c b/tests/sources/0204_assign_rand.c new file mode 100644 index 0000000..8bb9347 --- /dev/null +++ b/tests/sources/0204_assign_rand.c @@ -0,0 +1,3 @@ +int x; +x = rand(1,99); +print(x); diff --git a/tests/sources/0205_assign_rand2.c b/tests/sources/0205_assign_rand2.c new file mode 100644 index 0000000..a5aade7 --- /dev/null +++ b/tests/sources/0205_assign_rand2.c @@ -0,0 +1,3 @@ +int x; +x = rand(10,-5); +print(x); diff --git a/tests/sources/0206_assign_add.c b/tests/sources/0206_assign_add.c new file mode 100644 index 0000000..6c8dffe --- /dev/null +++ b/tests/sources/0206_assign_add.c @@ -0,0 +1,2 @@ +int x; +x = 2 + 5; diff --git a/tests/sources/0207_assign_add2.c b/tests/sources/0207_assign_add2.c new file mode 100644 index 0000000..1f8ec56 --- /dev/null +++ b/tests/sources/0207_assign_add2.c @@ -0,0 +1,2 @@ +int x; +x = rand(1,5) + rand (10,10); diff --git a/tests/sources/0208_assign_add3.c b/tests/sources/0208_assign_add3.c new file mode 100644 index 0000000..2f6357f --- /dev/null +++ b/tests/sources/0208_assign_add3.c @@ -0,0 +1,2 @@ +int x; +x = x + 2; diff --git a/tests/sources/0209_assign_neg.c b/tests/sources/0209_assign_neg.c new file mode 100644 index 0000000..f52fa2b --- /dev/null +++ b/tests/sources/0209_assign_neg.c @@ -0,0 +1,2 @@ +int x; +x = -9; diff --git a/tests/sources/0210_assign_neg2.c b/tests/sources/0210_assign_neg2.c new file mode 100644 index 0000000..d297b2c --- /dev/null +++ b/tests/sources/0210_assign_neg2.c @@ -0,0 +1,3 @@ +int x; +x = -rand(-1,10); + diff --git a/tests/sources/0211_assign_sub.c b/tests/sources/0211_assign_sub.c new file mode 100644 index 0000000..8f7b962 --- /dev/null +++ b/tests/sources/0211_assign_sub.c @@ -0,0 +1,2 @@ +int x; +x = 999 - 1; diff --git a/tests/sources/0212_assign_sub2.c b/tests/sources/0212_assign_sub2.c new file mode 100644 index 0000000..0b4f96f --- /dev/null +++ b/tests/sources/0212_assign_sub2.c @@ -0,0 +1,2 @@ +int x; +x = rand(1,10) - rand(2,3); diff --git a/tests/sources/0213_assign_mul.c b/tests/sources/0213_assign_mul.c new file mode 100644 index 0000000..6ba6b71 --- /dev/null +++ b/tests/sources/0213_assign_mul.c @@ -0,0 +1,2 @@ +int x; +x = 5 * 8; diff --git a/tests/sources/0214_assign_mul2.c b/tests/sources/0214_assign_mul2.c new file mode 100644 index 0000000..a5cdeef --- /dev/null +++ b/tests/sources/0214_assign_mul2.c @@ -0,0 +1,2 @@ +int x; +x = rand(1,3) * rand(2,9); diff --git a/tests/sources/0215_assign_mul3.c b/tests/sources/0215_assign_mul3.c new file mode 100644 index 0000000..b4affcf --- /dev/null +++ b/tests/sources/0215_assign_mul3.c @@ -0,0 +1,2 @@ +int x; +x = rand(-5,3) * rand(-1,10); diff --git a/tests/sources/0216_assign_mul4.c b/tests/sources/0216_assign_mul4.c new file mode 100644 index 0000000..7a10bb1 --- /dev/null +++ b/tests/sources/0216_assign_mul4.c @@ -0,0 +1,2 @@ +int x; +x = x * 0; diff --git a/tests/sources/0217_assign_copy.c b/tests/sources/0217_assign_copy.c new file mode 100644 index 0000000..bdff7a4 --- /dev/null +++ b/tests/sources/0217_assign_copy.c @@ -0,0 +1,5 @@ +int x; +int y; +x = 12; +y = x; +print(y); diff --git a/tests/sources/0218_assign_rel.c b/tests/sources/0218_assign_rel.c new file mode 100644 index 0000000..921d6ec --- /dev/null +++ b/tests/sources/0218_assign_rel.c @@ -0,0 +1,5 @@ +int x; +int y; +x = 15; +y = x + 2; +print(y); diff --git a/tests/sources/0219_assign_rel2.c b/tests/sources/0219_assign_rel2.c new file mode 100644 index 0000000..b19564d --- /dev/null +++ b/tests/sources/0219_assign_rel2.c @@ -0,0 +1,3 @@ +int x = rand(1,5); +int y = rand(2,10); +int z = x + 2*y; diff --git a/tests/sources/0300_if_true.c b/tests/sources/0300_if_true.c new file mode 100644 index 0000000..c824dbc --- /dev/null +++ b/tests/sources/0300_if_true.c @@ -0,0 +1,2 @@ +int x = 1; +if (1 <= 2) x = 9; diff --git a/tests/sources/0301_if_false.c b/tests/sources/0301_if_false.c new file mode 100644 index 0000000..6ce93de --- /dev/null +++ b/tests/sources/0301_if_false.c @@ -0,0 +1,2 @@ +int x = 1; +if (1 >= 2) x = 9; diff --git a/tests/sources/0302_if_both.c b/tests/sources/0302_if_both.c new file mode 100644 index 0000000..5afc2f8 --- /dev/null +++ b/tests/sources/0302_if_both.c @@ -0,0 +1,2 @@ +int x = 1; +if (rand(0,1) == 0) x = 9; diff --git a/tests/sources/0303_if_else_true.c b/tests/sources/0303_if_else_true.c new file mode 100644 index 0000000..8fa783f --- /dev/null +++ b/tests/sources/0303_if_else_true.c @@ -0,0 +1,2 @@ +int x = 1; +if (1 <= 2) x = 5; else x = 10; diff --git a/tests/sources/0304_if_else_false.c b/tests/sources/0304_if_else_false.c new file mode 100644 index 0000000..dab7fd2 --- /dev/null +++ b/tests/sources/0304_if_else_false.c @@ -0,0 +1,2 @@ +int x = 1; +if (1 >= 2) x = 5; else x = 10; diff --git a/tests/sources/0305_if_else_both.c b/tests/sources/0305_if_else_both.c new file mode 100644 index 0000000..ddf0eb2 --- /dev/null +++ b/tests/sources/0305_if_else_both.c @@ -0,0 +1,2 @@ +int x = 1; +if (rand(0,1) == 0) x = 5; else x = 10; diff --git a/tests/sources/0306_if_rel.c b/tests/sources/0306_if_rel.c new file mode 100644 index 0000000..66ddcc1 --- /dev/null +++ b/tests/sources/0306_if_rel.c @@ -0,0 +1,3 @@ +int x,y; +if (rand(0,1) == 0) { x = 1; y = 3; } +else { x = 2; y = 1; } diff --git a/tests/sources/0307_if_var.c b/tests/sources/0307_if_var.c new file mode 100644 index 0000000..a18b71b --- /dev/null +++ b/tests/sources/0307_if_var.c @@ -0,0 +1,3 @@ +int x = rand(-10,20); +if (x >= 0) { print(x); } +else { print(x); } diff --git a/tests/sources/0308_if_var2.c b/tests/sources/0308_if_var2.c new file mode 100644 index 0000000..cf3aa0f --- /dev/null +++ b/tests/sources/0308_if_var2.c @@ -0,0 +1,2 @@ +int x = rand(-20,10); +if (x < 2) x = -x; diff --git a/tests/sources/0309_if_var_rel.c b/tests/sources/0309_if_var_rel.c new file mode 100644 index 0000000..1788f99 --- /dev/null +++ b/tests/sources/0309_if_var_rel.c @@ -0,0 +1,3 @@ +int x = rand(-10,25); +int y = rand(-15,20); +if (x >= y) x = y; diff --git a/tests/sources/0310_cmp_le.c b/tests/sources/0310_cmp_le.c new file mode 100644 index 0000000..5340ed4 --- /dev/null +++ b/tests/sources/0310_cmp_le.c @@ -0,0 +1,3 @@ +int x = rand(10,20); +int y = rand(15,30); +if (x <= y) print(x,y); diff --git a/tests/sources/0311_cmp_le2.c b/tests/sources/0311_cmp_le2.c new file mode 100644 index 0000000..d88fb3b --- /dev/null +++ b/tests/sources/0311_cmp_le2.c @@ -0,0 +1,3 @@ +int x = rand(10,20); +int y = rand(8,17); +if (x <= y) print(x,y); diff --git a/tests/sources/0312_cmp_le3.c b/tests/sources/0312_cmp_le3.c new file mode 100644 index 0000000..00c4b32 --- /dev/null +++ b/tests/sources/0312_cmp_le3.c @@ -0,0 +1,3 @@ +int y = rand(10,20); +int x = rand(30,55); +if (x <= y) print(x); diff --git a/tests/sources/0313_cmp_lt.c b/tests/sources/0313_cmp_lt.c new file mode 100644 index 0000000..794fdd8 --- /dev/null +++ b/tests/sources/0313_cmp_lt.c @@ -0,0 +1,3 @@ +int x = rand(10,20); +int y = rand(5,15); +if (x < y) print(x,y); diff --git a/tests/sources/0314_cmp_ge.c b/tests/sources/0314_cmp_ge.c new file mode 100644 index 0000000..11ccae5 --- /dev/null +++ b/tests/sources/0314_cmp_ge.c @@ -0,0 +1,3 @@ +int x = rand(10,20); +int y = rand(15,30); +if (x >= y) print(x,y); diff --git a/tests/sources/0315_cmp_gt.c b/tests/sources/0315_cmp_gt.c new file mode 100644 index 0000000..2ab9e11 --- /dev/null +++ b/tests/sources/0315_cmp_gt.c @@ -0,0 +1,3 @@ +int x = rand(10,20); +int y = rand(15,30); +if (x > y) print(x,y); diff --git a/tests/sources/0316_cmp_eq.c b/tests/sources/0316_cmp_eq.c new file mode 100644 index 0000000..3fe7b2e --- /dev/null +++ b/tests/sources/0316_cmp_eq.c @@ -0,0 +1,3 @@ +int x = rand(15,30); +int y = rand(10,20); +if (x == y) print(x,y); diff --git a/tests/sources/0317_cmp_eq2.c b/tests/sources/0317_cmp_eq2.c new file mode 100644 index 0000000..5d3b677 --- /dev/null +++ b/tests/sources/0317_cmp_eq2.c @@ -0,0 +1,3 @@ +int x = rand(15,20); +int y = rand(25,30); +if (x == y) print(x,y); diff --git a/tests/sources/0318_cmp_ne.c b/tests/sources/0318_cmp_ne.c new file mode 100644 index 0000000..8e7bf10 --- /dev/null +++ b/tests/sources/0318_cmp_ne.c @@ -0,0 +1,3 @@ +int x = rand(10,15); +int y = rand(10,15); +if (x != y) print(x,y); diff --git a/tests/sources/0319_cmp_ne.c b/tests/sources/0319_cmp_ne.c new file mode 100644 index 0000000..3dbe18b --- /dev/null +++ b/tests/sources/0319_cmp_ne.c @@ -0,0 +1,3 @@ +int x = rand(10,15); +int y = 10; +if (x != y) print(x,y); diff --git a/tests/sources/0320_cmp_eq_ne.c b/tests/sources/0320_cmp_eq_ne.c new file mode 100644 index 0000000..6f4244c --- /dev/null +++ b/tests/sources/0320_cmp_eq_ne.c @@ -0,0 +1,5 @@ +int x = rand(10,15); +int y = 10; +if (x == y) print(x,y); +else print(x,y); + diff --git a/tests/sources/0321_cmp_rel.c b/tests/sources/0321_cmp_rel.c new file mode 100644 index 0000000..d9c973c --- /dev/null +++ b/tests/sources/0321_cmp_rel.c @@ -0,0 +1,3 @@ +int x = rand(10,20); +int y = x; +if (x >= 15) { print(y); } diff --git a/tests/sources/0322_if_and.c b/tests/sources/0322_if_and.c new file mode 100644 index 0000000..cd10203 --- /dev/null +++ b/tests/sources/0322_if_and.c @@ -0,0 +1,4 @@ +int x = rand(10,20); +int y = rand(30,40); +if (x>=15 && y>=35) { print(x,y); } +else { print(x,y); } diff --git a/tests/sources/0323_if_or.c b/tests/sources/0323_if_or.c new file mode 100644 index 0000000..145983e --- /dev/null +++ b/tests/sources/0323_if_or.c @@ -0,0 +1,4 @@ +int x = rand(10,20); +int y = rand(30,40); +if (x>=15 || y>=35) { print(x,y); } +else { print(x,y); } diff --git a/tests/sources/0324_if_not.c b/tests/sources/0324_if_not.c new file mode 100644 index 0000000..8a6abb7 --- /dev/null +++ b/tests/sources/0324_if_not.c @@ -0,0 +1,4 @@ +int x = rand(10,20); +int y = rand(30,40); +if (!(x>=15) || y>=35) { print(x,y); } +else { print(x,y); } diff --git a/tests/sources/0325_if_bool.c b/tests/sources/0325_if_bool.c new file mode 100644 index 0000000..614d5d7 --- /dev/null +++ b/tests/sources/0325_if_bool.c @@ -0,0 +1,4 @@ +int x = rand(10,20); +int y = rand(10,20); +if (x<=15 && y>=15 || x>=15 && y<=15) { print(x,y); } +else { print(x,y); } diff --git a/tests/sources/0400_assert_true.c b/tests/sources/0400_assert_true.c new file mode 100644 index 0000000..6516bac --- /dev/null +++ b/tests/sources/0400_assert_true.c @@ -0,0 +1,2 @@ +int x = 2; +assert(x>=1); diff --git a/tests/sources/0401_assert_false.c b/tests/sources/0401_assert_false.c new file mode 100644 index 0000000..b2bc702 --- /dev/null +++ b/tests/sources/0401_assert_false.c @@ -0,0 +1,2 @@ +int x = 9; +assert (x < 5); diff --git a/tests/sources/0402_assert_both.c b/tests/sources/0402_assert_both.c new file mode 100644 index 0000000..f9afd61 --- /dev/null +++ b/tests/sources/0402_assert_both.c @@ -0,0 +1,3 @@ +int x = rand (-5,10); +assert(x >= 0); +assert(x > 0); diff --git a/tests/sources/0403_assert_both2.c b/tests/sources/0403_assert_both2.c new file mode 100644 index 0000000..1a35775 --- /dev/null +++ b/tests/sources/0403_assert_both2.c @@ -0,0 +1,3 @@ +int x = rand (-5,10); +assert(x > 0); +assert(x >= 0); diff --git a/tests/sources/0404_assert_rel.c b/tests/sources/0404_assert_rel.c new file mode 100644 index 0000000..933d005 --- /dev/null +++ b/tests/sources/0404_assert_rel.c @@ -0,0 +1,4 @@ +int x,y; +if (rand(0,1)==0) { x = 1; y = 1; } +else { x = 3 ; y = 3; } +assert(x==y); diff --git a/tests/sources/0500_loop_count.c b/tests/sources/0500_loop_count.c new file mode 100644 index 0000000..ace98cf --- /dev/null +++ b/tests/sources/0500_loop_count.c @@ -0,0 +1,5 @@ +int x = 0; +while (x < 100) { + print(x); + x = x + 1; +} diff --git a/tests/sources/0501_loop_infinite.c b/tests/sources/0501_loop_infinite.c new file mode 100644 index 0000000..2676685 --- /dev/null +++ b/tests/sources/0501_loop_infinite.c @@ -0,0 +1,4 @@ +int x = 0; +while (x < 10) { + print(x); +} diff --git a/tests/sources/0502_loop_infinite2.c b/tests/sources/0502_loop_infinite2.c new file mode 100644 index 0000000..ef899a4 --- /dev/null +++ b/tests/sources/0502_loop_infinite2.c @@ -0,0 +1,5 @@ +int x = 0; +while (x < 100) { + print(x); + x = x - 1; +} diff --git a/tests/sources/0503_loop_nondet.c b/tests/sources/0503_loop_nondet.c new file mode 100644 index 0000000..ab17b7b --- /dev/null +++ b/tests/sources/0503_loop_nondet.c @@ -0,0 +1,5 @@ +int x = 0; +while (rand(0,1) == 0) { + print(x); + x = x + 1; +} diff --git a/tests/sources/0504_loop_rel.c b/tests/sources/0504_loop_rel.c new file mode 100644 index 0000000..05804af --- /dev/null +++ b/tests/sources/0504_loop_rel.c @@ -0,0 +1,7 @@ +int N = rand(0,1000); +int x = 0; +while (x < N) { + print(x,N); + x = x + 1; +} +assert(x==N); diff --git a/tests/sources/0505_loop_rel2.c b/tests/sources/0505_loop_rel2.c new file mode 100644 index 0000000..e335932 --- /dev/null +++ b/tests/sources/0505_loop_rel2.c @@ -0,0 +1,7 @@ +int N = rand(0,1000); +int x = 0; +while (x < N) { + print(x,N); + x = x + rand(0,3); +} +assert(x>=N && x<N+3); diff --git a/tests/sources/0506_loop_limit.c b/tests/sources/0506_loop_limit.c new file mode 100644 index 0000000..1a0d4f7 --- /dev/null +++ b/tests/sources/0506_loop_limit.c @@ -0,0 +1,5 @@ +int x = 0; +while (rand(0,1)==0) { + if (x < 10000) x = x + 1; +} +print(x); diff --git a/tests/sources/0507_loop_limit2.c b/tests/sources/0507_loop_limit2.c new file mode 100644 index 0000000..bafdf77 --- /dev/null +++ b/tests/sources/0507_loop_limit2.c @@ -0,0 +1,6 @@ +int x = 0; +int N = rand(0,1000); +while (rand(0,1)==0) { + if (x < N) x = x + 1; +} +print(x); diff --git a/tests/sources/0508_loop_init.c b/tests/sources/0508_loop_init.c new file mode 100644 index 0000000..f0817e5 --- /dev/null +++ b/tests/sources/0508_loop_init.c @@ -0,0 +1,14 @@ +int init; +int x; + +init = 0; +while (rand(0,1)==0) { + if (init == 0) { + x = 0; + init = 1; + } + else { + x = x + 1; + } + assert(x >= 0); +} diff --git a/tests/sources/0509_loop_nested.c b/tests/sources/0509_loop_nested.c new file mode 100644 index 0000000..54d5be6 --- /dev/null +++ b/tests/sources/0509_loop_nested.c @@ -0,0 +1,9 @@ +int i=0, j=0; + +while (i < 1000) { + j = 0; + while (j < i) { + j = j + 1; + } + i = i + 1; +} diff --git a/tests/sources/0510_loop_nested2.c b/tests/sources/0510_loop_nested2.c new file mode 100644 index 0000000..90c52ec --- /dev/null +++ b/tests/sources/0510_loop_nested2.c @@ -0,0 +1,10 @@ +int i,j; + +i = 0; +while (i < 1000) { + j = 0; + while (j < i) { + j = j + 1; + } + i = i + 1; +} diff --git a/tests/sources/0600_bubble_sort.c b/tests/sources/0600_bubble_sort.c new file mode 100644 index 0000000..5cad03d --- /dev/null +++ b/tests/sources/0600_bubble_sort.c @@ -0,0 +1,32 @@ +// Example from Cousot Habwachs POPL 1978 + +// Bubble sort, where array operations are abstracted away +// to get a non-deterministic scalar program + +// expected results: +// - with polyhedra, no assertion failure (proof of absence of array overflow) +// - with intervals, assertion failure + +int B,J,T; +int N = rand(0,100000); // array size + +B = N; +while (B >= 1) { + J = 1; + T = 0; + while (J <= B-1) { + + // array bound-check + assert(1 <= J && J <= N); + assert(1 <= (J+1) && (J+1) <= N); + + // the non-deterministic test models comparing TAB[J] and TAB[J+1] + if (rand(0,1)==0) { + // where, we would exchange TAB[J] and TAB[J+1]; + T = J; + } + + J = J + 1; + } + B = T; +} diff --git a/tests/sources/0601_heap_sort.c b/tests/sources/0601_heap_sort.c new file mode 100644 index 0000000..dd12e1a --- /dev/null +++ b/tests/sources/0601_heap_sort.c @@ -0,0 +1,66 @@ +// Example from Cousot Habwachs POPL 1978 + +// Heap sort, where array operations are abstracted away +// to get a non-deterministic scalar program + +// expected results: with polyhedra, no assertion failure + +int L,R,I,J; +int N = rand(1,100000); // array size + +L = N/2 + 1; +R = N; + +if (L >= 2) { + L = L - 1; + // model the assignment "K = TAB[L]" + assert(1 <= L && L <= N); +} +else { + // model the assignments "K = TAB[R]; TAB[R] = TAB[1]" + assert(1 <= R && R <= N); + assert(1 <= 1 && 1 <= N); + R = R - 1; +} + +while (R >= 2) { + I = L; + J = 2*I; + + while (J <= R && rand(0,1)==0) { + if (J <= R-1) { + // model the comparison "TAB[J] < TAB[J+1]" + assert(1 <= J && J <= N); + assert(1 <= (J+1) && (J+1) <= N); + if (rand(0,1)==0) { J = J + 1; } + } + + // model the comparison "K < TAB[J]" + assert(1 <= J && J <= N); + if (rand(0,1)==0) { + // model the assignment "TAB[I] = TAB[J]" + assert(1 <= I && I <= N); + assert(1 <= J && J <= N); + I = J; + J = 2*J; + } + } + + // model the assignment "TAB[I] = K" + assert(1 <= I && I <= N); + + if (L >= 2) { + L = L - 1; + // model the assignment "K = TAB[L]" + assert(1 <= L && L <= N); + } + else { + // model the assignments "K = TAB[R]; TAB[R] = TAB[1]" + assert(1 <= R && R <= N); + assert(1 <= 1 && 1 <= N); + R = R - 1; + } + + // model the assignment "TAB[1] = K" + assert(1 <= 1 && 1 <= N); +} diff --git a/tests/sources/0602_rate_limiter.c b/tests/sources/0602_rate_limiter.c new file mode 100644 index 0000000..a36da77 --- /dev/null +++ b/tests/sources/0602_rate_limiter.c @@ -0,0 +1,26 @@ +// Example from Miné HOSC 2006 + +// Rate limiter: at each loop iteration, a new input is fetched (X) and +// a new output (Y) is computed; Y tries to follow X but is limited to +// change no more that a given slope (D) in absolute value + +// To prove that the assertion holds, this version needs the polyhedra +// domain and an unrolling factor of at least 6 + +int X; // input +int Y; // output +int S; // last output +int D; // maximum slope; + +Y = 0; +while (rand(0,1)==1) { + X = rand(-128,128); + D = rand(0,16); + S = Y; + int R = X - S; // current slope + Y = X; + if (R <= -D) Y = S - D; // slope too small + else if (R >= D) Y = S + D; // slope too large +} + +assert(Y >= -128 && Y <= 128); diff --git a/tests/sources/0603_rate_limiter2.c b/tests/sources/0603_rate_limiter2.c new file mode 100644 index 0000000..32a7a17 --- /dev/null +++ b/tests/sources/0603_rate_limiter2.c @@ -0,0 +1,21 @@ +// This version is similar to the previous one, but the assertion is checked +// inside the loop +// No unrolling is necessary in this version! + +int X; // input +int Y; // output +int S; // last output +int D; // maximum slope; + +Y = 0; +while (rand(0,1)==1) { + X = rand(-128,128); + D = rand(0,16); + S = Y; + int R = X - S; // current slope + Y = X; + if (R <= -D) Y = S - D; // slope too small + else if (R >= D) Y = S + D; // slope too large + + assert(Y >= -128 && Y <= 128); +} |