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] ]
-------------------------------------
