diff options
Diffstat (limited to 'tests/results')
228 files changed, 3955 insertions, 0 deletions
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|] + +------------------------------------- + |