diff options
Diffstat (limited to 'tests/sources')
75 files changed, 396 insertions, 0 deletions
diff --git a/tests/sources/0000_noinit_var.c b/tests/sources/0000_noinit_var.c new file mode 100644 index 0000000..6d1a0d4 --- /dev/null +++ b/tests/sources/0000_noinit_var.c @@ -0,0 +1 @@ +int x; diff --git a/tests/sources/0001_noinit_2var.c b/tests/sources/0001_noinit_2var.c new file mode 100644 index 0000000..2b9d16b --- /dev/null +++ b/tests/sources/0001_noinit_2var.c @@ -0,0 +1,2 @@ +int x; +int y; diff --git a/tests/sources/0002_init_var.c b/tests/sources/0002_init_var.c new file mode 100644 index 0000000..15bfa8f --- /dev/null +++ b/tests/sources/0002_init_var.c @@ -0,0 +1 @@ +int x = 0; diff --git a/tests/sources/0003_init_2var.c b/tests/sources/0003_init_2var.c new file mode 100644 index 0000000..83aefaf --- /dev/null +++ b/tests/sources/0003_init_2var.c @@ -0,0 +1,2 @@ +int x = 0; +int y = 1; diff --git a/tests/sources/0004_init_2var2.c b/tests/sources/0004_init_2var2.c new file mode 100644 index 0000000..f81c09c --- /dev/null +++ b/tests/sources/0004_init_2var2.c @@ -0,0 +1 @@ +int x = 9, y = 12; diff --git a/tests/sources/0100_print_var.c b/tests/sources/0100_print_var.c new file mode 100644 index 0000000..e2f9464 --- /dev/null +++ b/tests/sources/0100_print_var.c @@ -0,0 +1,2 @@ +int x = 2; +print(x); diff --git a/tests/sources/0101_print_2var.c b/tests/sources/0101_print_2var.c new file mode 100644 index 0000000..92aa4a9 --- /dev/null +++ b/tests/sources/0101_print_2var.c @@ -0,0 +1,3 @@ +int x = 3; +int y = 15; +print(y); diff --git a/tests/sources/0102_print_3var.c b/tests/sources/0102_print_3var.c new file mode 100644 index 0000000..81fe534 --- /dev/null +++ b/tests/sources/0102_print_3var.c @@ -0,0 +1,4 @@ +int x = 3; +int y = 15; +int z = 99; +print(z,x); diff --git a/tests/sources/0103_local.c b/tests/sources/0103_local.c new file mode 100644 index 0000000..c6683be --- /dev/null +++ b/tests/sources/0103_local.c @@ -0,0 +1,5 @@ +int x = 12; +{ + int y = 9; + print(x,y); +} diff --git a/tests/sources/0200_assign_cst.c b/tests/sources/0200_assign_cst.c new file mode 100644 index 0000000..8340469 --- /dev/null +++ b/tests/sources/0200_assign_cst.c @@ -0,0 +1,6 @@ +int x; +print(x); +x = 12; +print(x); +x = 15; +print(x); diff --git a/tests/sources/0201_assign_cst2.c b/tests/sources/0201_assign_cst2.c new file mode 100644 index 0000000..6f28061 --- /dev/null +++ b/tests/sources/0201_assign_cst2.c @@ -0,0 +1,7 @@ +int x, y; +print(x,y); +x = 12; +print(x,y); +y = 15; +x = 99; +print(x,y); diff --git a/tests/sources/0202_assign_expr.c b/tests/sources/0202_assign_expr.c new file mode 100644 index 0000000..7d16636 --- /dev/null +++ b/tests/sources/0202_assign_expr.c @@ -0,0 +1,2 @@ +int x; +x = 2 + 2; diff --git a/tests/sources/0203_assign_expr2.c b/tests/sources/0203_assign_expr2.c new file mode 100644 index 0000000..7583362 --- /dev/null +++ b/tests/sources/0203_assign_expr2.c @@ -0,0 +1,5 @@ +int x,y; +x = 12; +y = 16; +x = x + y + 2; +print(x); diff --git a/tests/sources/0204_assign_rand.c b/tests/sources/0204_assign_rand.c new file mode 100644 index 0000000..8bb9347 --- /dev/null +++ b/tests/sources/0204_assign_rand.c @@ -0,0 +1,3 @@ +int x; +x = rand(1,99); +print(x); diff --git a/tests/sources/0205_assign_rand2.c b/tests/sources/0205_assign_rand2.c new file mode 100644 index 0000000..a5aade7 --- /dev/null +++ b/tests/sources/0205_assign_rand2.c @@ -0,0 +1,3 @@ +int x; +x = rand(10,-5); +print(x); diff --git a/tests/sources/0206_assign_add.c b/tests/sources/0206_assign_add.c new file mode 100644 index 0000000..6c8dffe --- /dev/null +++ b/tests/sources/0206_assign_add.c @@ -0,0 +1,2 @@ +int x; +x = 2 + 5; diff --git a/tests/sources/0207_assign_add2.c b/tests/sources/0207_assign_add2.c new file mode 100644 index 0000000..1f8ec56 --- /dev/null +++ b/tests/sources/0207_assign_add2.c @@ -0,0 +1,2 @@ +int x; +x = rand(1,5) + rand (10,10); diff --git a/tests/sources/0208_assign_add3.c b/tests/sources/0208_assign_add3.c new file mode 100644 index 0000000..2f6357f --- /dev/null +++ b/tests/sources/0208_assign_add3.c @@ -0,0 +1,2 @@ +int x; +x = x + 2; diff --git a/tests/sources/0209_assign_neg.c b/tests/sources/0209_assign_neg.c new file mode 100644 index 0000000..f52fa2b --- /dev/null +++ b/tests/sources/0209_assign_neg.c @@ -0,0 +1,2 @@ +int x; +x = -9; diff --git a/tests/sources/0210_assign_neg2.c b/tests/sources/0210_assign_neg2.c new file mode 100644 index 0000000..d297b2c --- /dev/null +++ b/tests/sources/0210_assign_neg2.c @@ -0,0 +1,3 @@ +int x; +x = -rand(-1,10); + diff --git a/tests/sources/0211_assign_sub.c b/tests/sources/0211_assign_sub.c new file mode 100644 index 0000000..8f7b962 --- /dev/null +++ b/tests/sources/0211_assign_sub.c @@ -0,0 +1,2 @@ +int x; +x = 999 - 1; diff --git a/tests/sources/0212_assign_sub2.c b/tests/sources/0212_assign_sub2.c new file mode 100644 index 0000000..0b4f96f --- /dev/null +++ b/tests/sources/0212_assign_sub2.c @@ -0,0 +1,2 @@ +int x; +x = rand(1,10) - rand(2,3); diff --git a/tests/sources/0213_assign_mul.c b/tests/sources/0213_assign_mul.c new file mode 100644 index 0000000..6ba6b71 --- /dev/null +++ b/tests/sources/0213_assign_mul.c @@ -0,0 +1,2 @@ +int x; +x = 5 * 8; diff --git a/tests/sources/0214_assign_mul2.c b/tests/sources/0214_assign_mul2.c new file mode 100644 index 0000000..a5cdeef --- /dev/null +++ b/tests/sources/0214_assign_mul2.c @@ -0,0 +1,2 @@ +int x; +x = rand(1,3) * rand(2,9); diff --git a/tests/sources/0215_assign_mul3.c b/tests/sources/0215_assign_mul3.c new file mode 100644 index 0000000..b4affcf --- /dev/null +++ b/tests/sources/0215_assign_mul3.c @@ -0,0 +1,2 @@ +int x; +x = rand(-5,3) * rand(-1,10); diff --git a/tests/sources/0216_assign_mul4.c b/tests/sources/0216_assign_mul4.c new file mode 100644 index 0000000..7a10bb1 --- /dev/null +++ b/tests/sources/0216_assign_mul4.c @@ -0,0 +1,2 @@ +int x; +x = x * 0; diff --git a/tests/sources/0217_assign_copy.c b/tests/sources/0217_assign_copy.c new file mode 100644 index 0000000..bdff7a4 --- /dev/null +++ b/tests/sources/0217_assign_copy.c @@ -0,0 +1,5 @@ +int x; +int y; +x = 12; +y = x; +print(y); diff --git a/tests/sources/0218_assign_rel.c b/tests/sources/0218_assign_rel.c new file mode 100644 index 0000000..921d6ec --- /dev/null +++ b/tests/sources/0218_assign_rel.c @@ -0,0 +1,5 @@ +int x; +int y; +x = 15; +y = x + 2; +print(y); diff --git a/tests/sources/0219_assign_rel2.c b/tests/sources/0219_assign_rel2.c new file mode 100644 index 0000000..b19564d --- /dev/null +++ b/tests/sources/0219_assign_rel2.c @@ -0,0 +1,3 @@ +int x = rand(1,5); +int y = rand(2,10); +int z = x + 2*y; diff --git a/tests/sources/0300_if_true.c b/tests/sources/0300_if_true.c new file mode 100644 index 0000000..c824dbc --- /dev/null +++ b/tests/sources/0300_if_true.c @@ -0,0 +1,2 @@ +int x = 1; +if (1 <= 2) x = 9; diff --git a/tests/sources/0301_if_false.c b/tests/sources/0301_if_false.c new file mode 100644 index 0000000..6ce93de --- /dev/null +++ b/tests/sources/0301_if_false.c @@ -0,0 +1,2 @@ +int x = 1; +if (1 >= 2) x = 9; diff --git a/tests/sources/0302_if_both.c b/tests/sources/0302_if_both.c new file mode 100644 index 0000000..5afc2f8 --- /dev/null +++ b/tests/sources/0302_if_both.c @@ -0,0 +1,2 @@ +int x = 1; +if (rand(0,1) == 0) x = 9; diff --git a/tests/sources/0303_if_else_true.c b/tests/sources/0303_if_else_true.c new file mode 100644 index 0000000..8fa783f --- /dev/null +++ b/tests/sources/0303_if_else_true.c @@ -0,0 +1,2 @@ +int x = 1; +if (1 <= 2) x = 5; else x = 10; diff --git a/tests/sources/0304_if_else_false.c b/tests/sources/0304_if_else_false.c new file mode 100644 index 0000000..dab7fd2 --- /dev/null +++ b/tests/sources/0304_if_else_false.c @@ -0,0 +1,2 @@ +int x = 1; +if (1 >= 2) x = 5; else x = 10; diff --git a/tests/sources/0305_if_else_both.c b/tests/sources/0305_if_else_both.c new file mode 100644 index 0000000..ddf0eb2 --- /dev/null +++ b/tests/sources/0305_if_else_both.c @@ -0,0 +1,2 @@ +int x = 1; +if (rand(0,1) == 0) x = 5; else x = 10; diff --git a/tests/sources/0306_if_rel.c b/tests/sources/0306_if_rel.c new file mode 100644 index 0000000..66ddcc1 --- /dev/null +++ b/tests/sources/0306_if_rel.c @@ -0,0 +1,3 @@ +int x,y; +if (rand(0,1) == 0) { x = 1; y = 3; } +else { x = 2; y = 1; } diff --git a/tests/sources/0307_if_var.c b/tests/sources/0307_if_var.c new file mode 100644 index 0000000..a18b71b --- /dev/null +++ b/tests/sources/0307_if_var.c @@ -0,0 +1,3 @@ +int x = rand(-10,20); +if (x >= 0) { print(x); } +else { print(x); } diff --git a/tests/sources/0308_if_var2.c b/tests/sources/0308_if_var2.c new file mode 100644 index 0000000..cf3aa0f --- /dev/null +++ b/tests/sources/0308_if_var2.c @@ -0,0 +1,2 @@ +int x = rand(-20,10); +if (x < 2) x = -x; diff --git a/tests/sources/0309_if_var_rel.c b/tests/sources/0309_if_var_rel.c new file mode 100644 index 0000000..1788f99 --- /dev/null +++ b/tests/sources/0309_if_var_rel.c @@ -0,0 +1,3 @@ +int x = rand(-10,25); +int y = rand(-15,20); +if (x >= y) x = y; diff --git a/tests/sources/0310_cmp_le.c b/tests/sources/0310_cmp_le.c new file mode 100644 index 0000000..5340ed4 --- /dev/null +++ b/tests/sources/0310_cmp_le.c @@ -0,0 +1,3 @@ +int x = rand(10,20); +int y = rand(15,30); +if (x <= y) print(x,y); diff --git a/tests/sources/0311_cmp_le2.c b/tests/sources/0311_cmp_le2.c new file mode 100644 index 0000000..d88fb3b --- /dev/null +++ b/tests/sources/0311_cmp_le2.c @@ -0,0 +1,3 @@ +int x = rand(10,20); +int y = rand(8,17); +if (x <= y) print(x,y); diff --git a/tests/sources/0312_cmp_le3.c b/tests/sources/0312_cmp_le3.c new file mode 100644 index 0000000..00c4b32 --- /dev/null +++ b/tests/sources/0312_cmp_le3.c @@ -0,0 +1,3 @@ +int y = rand(10,20); +int x = rand(30,55); +if (x <= y) print(x); diff --git a/tests/sources/0313_cmp_lt.c b/tests/sources/0313_cmp_lt.c new file mode 100644 index 0000000..794fdd8 --- /dev/null +++ b/tests/sources/0313_cmp_lt.c @@ -0,0 +1,3 @@ +int x = rand(10,20); +int y = rand(5,15); +if (x < y) print(x,y); diff --git a/tests/sources/0314_cmp_ge.c b/tests/sources/0314_cmp_ge.c new file mode 100644 index 0000000..11ccae5 --- /dev/null +++ b/tests/sources/0314_cmp_ge.c @@ -0,0 +1,3 @@ +int x = rand(10,20); +int y = rand(15,30); +if (x >= y) print(x,y); diff --git a/tests/sources/0315_cmp_gt.c b/tests/sources/0315_cmp_gt.c new file mode 100644 index 0000000..2ab9e11 --- /dev/null +++ b/tests/sources/0315_cmp_gt.c @@ -0,0 +1,3 @@ +int x = rand(10,20); +int y = rand(15,30); +if (x > y) print(x,y); diff --git a/tests/sources/0316_cmp_eq.c b/tests/sources/0316_cmp_eq.c new file mode 100644 index 0000000..3fe7b2e --- /dev/null +++ b/tests/sources/0316_cmp_eq.c @@ -0,0 +1,3 @@ +int x = rand(15,30); +int y = rand(10,20); +if (x == y) print(x,y); diff --git a/tests/sources/0317_cmp_eq2.c b/tests/sources/0317_cmp_eq2.c new file mode 100644 index 0000000..5d3b677 --- /dev/null +++ b/tests/sources/0317_cmp_eq2.c @@ -0,0 +1,3 @@ +int x = rand(15,20); +int y = rand(25,30); +if (x == y) print(x,y); diff --git a/tests/sources/0318_cmp_ne.c b/tests/sources/0318_cmp_ne.c new file mode 100644 index 0000000..8e7bf10 --- /dev/null +++ b/tests/sources/0318_cmp_ne.c @@ -0,0 +1,3 @@ +int x = rand(10,15); +int y = rand(10,15); +if (x != y) print(x,y); diff --git a/tests/sources/0319_cmp_ne.c b/tests/sources/0319_cmp_ne.c new file mode 100644 index 0000000..3dbe18b --- /dev/null +++ b/tests/sources/0319_cmp_ne.c @@ -0,0 +1,3 @@ +int x = rand(10,15); +int y = 10; +if (x != y) print(x,y); diff --git a/tests/sources/0320_cmp_eq_ne.c b/tests/sources/0320_cmp_eq_ne.c new file mode 100644 index 0000000..6f4244c --- /dev/null +++ b/tests/sources/0320_cmp_eq_ne.c @@ -0,0 +1,5 @@ +int x = rand(10,15); +int y = 10; +if (x == y) print(x,y); +else print(x,y); + diff --git a/tests/sources/0321_cmp_rel.c b/tests/sources/0321_cmp_rel.c new file mode 100644 index 0000000..d9c973c --- /dev/null +++ b/tests/sources/0321_cmp_rel.c @@ -0,0 +1,3 @@ +int x = rand(10,20); +int y = x; +if (x >= 15) { print(y); } diff --git a/tests/sources/0322_if_and.c b/tests/sources/0322_if_and.c new file mode 100644 index 0000000..cd10203 --- /dev/null +++ b/tests/sources/0322_if_and.c @@ -0,0 +1,4 @@ +int x = rand(10,20); +int y = rand(30,40); +if (x>=15 && y>=35) { print(x,y); } +else { print(x,y); } diff --git a/tests/sources/0323_if_or.c b/tests/sources/0323_if_or.c new file mode 100644 index 0000000..145983e --- /dev/null +++ b/tests/sources/0323_if_or.c @@ -0,0 +1,4 @@ +int x = rand(10,20); +int y = rand(30,40); +if (x>=15 || y>=35) { print(x,y); } +else { print(x,y); } diff --git a/tests/sources/0324_if_not.c b/tests/sources/0324_if_not.c new file mode 100644 index 0000000..8a6abb7 --- /dev/null +++ b/tests/sources/0324_if_not.c @@ -0,0 +1,4 @@ +int x = rand(10,20); +int y = rand(30,40); +if (!(x>=15) || y>=35) { print(x,y); } +else { print(x,y); } diff --git a/tests/sources/0325_if_bool.c b/tests/sources/0325_if_bool.c new file mode 100644 index 0000000..614d5d7 --- /dev/null +++ b/tests/sources/0325_if_bool.c @@ -0,0 +1,4 @@ +int x = rand(10,20); +int y = rand(10,20); +if (x<=15 && y>=15 || x>=15 && y<=15) { print(x,y); } +else { print(x,y); } diff --git a/tests/sources/0400_assert_true.c b/tests/sources/0400_assert_true.c new file mode 100644 index 0000000..6516bac --- /dev/null +++ b/tests/sources/0400_assert_true.c @@ -0,0 +1,2 @@ +int x = 2; +assert(x>=1); diff --git a/tests/sources/0401_assert_false.c b/tests/sources/0401_assert_false.c new file mode 100644 index 0000000..b2bc702 --- /dev/null +++ b/tests/sources/0401_assert_false.c @@ -0,0 +1,2 @@ +int x = 9; +assert (x < 5); diff --git a/tests/sources/0402_assert_both.c b/tests/sources/0402_assert_both.c new file mode 100644 index 0000000..f9afd61 --- /dev/null +++ b/tests/sources/0402_assert_both.c @@ -0,0 +1,3 @@ +int x = rand (-5,10); +assert(x >= 0); +assert(x > 0); diff --git a/tests/sources/0403_assert_both2.c b/tests/sources/0403_assert_both2.c new file mode 100644 index 0000000..1a35775 --- /dev/null +++ b/tests/sources/0403_assert_both2.c @@ -0,0 +1,3 @@ +int x = rand (-5,10); +assert(x > 0); +assert(x >= 0); diff --git a/tests/sources/0404_assert_rel.c b/tests/sources/0404_assert_rel.c new file mode 100644 index 0000000..933d005 --- /dev/null +++ b/tests/sources/0404_assert_rel.c @@ -0,0 +1,4 @@ +int x,y; +if (rand(0,1)==0) { x = 1; y = 1; } +else { x = 3 ; y = 3; } +assert(x==y); diff --git a/tests/sources/0500_loop_count.c b/tests/sources/0500_loop_count.c new file mode 100644 index 0000000..ace98cf --- /dev/null +++ b/tests/sources/0500_loop_count.c @@ -0,0 +1,5 @@ +int x = 0; +while (x < 100) { + print(x); + x = x + 1; +} diff --git a/tests/sources/0501_loop_infinite.c b/tests/sources/0501_loop_infinite.c new file mode 100644 index 0000000..2676685 --- /dev/null +++ b/tests/sources/0501_loop_infinite.c @@ -0,0 +1,4 @@ +int x = 0; +while (x < 10) { + print(x); +} diff --git a/tests/sources/0502_loop_infinite2.c b/tests/sources/0502_loop_infinite2.c new file mode 100644 index 0000000..ef899a4 --- /dev/null +++ b/tests/sources/0502_loop_infinite2.c @@ -0,0 +1,5 @@ +int x = 0; +while (x < 100) { + print(x); + x = x - 1; +} diff --git a/tests/sources/0503_loop_nondet.c b/tests/sources/0503_loop_nondet.c new file mode 100644 index 0000000..ab17b7b --- /dev/null +++ b/tests/sources/0503_loop_nondet.c @@ -0,0 +1,5 @@ +int x = 0; +while (rand(0,1) == 0) { + print(x); + x = x + 1; +} diff --git a/tests/sources/0504_loop_rel.c b/tests/sources/0504_loop_rel.c new file mode 100644 index 0000000..05804af --- /dev/null +++ b/tests/sources/0504_loop_rel.c @@ -0,0 +1,7 @@ +int N = rand(0,1000); +int x = 0; +while (x < N) { + print(x,N); + x = x + 1; +} +assert(x==N); diff --git a/tests/sources/0505_loop_rel2.c b/tests/sources/0505_loop_rel2.c new file mode 100644 index 0000000..e335932 --- /dev/null +++ b/tests/sources/0505_loop_rel2.c @@ -0,0 +1,7 @@ +int N = rand(0,1000); +int x = 0; +while (x < N) { + print(x,N); + x = x + rand(0,3); +} +assert(x>=N && x<N+3); diff --git a/tests/sources/0506_loop_limit.c b/tests/sources/0506_loop_limit.c new file mode 100644 index 0000000..1a0d4f7 --- /dev/null +++ b/tests/sources/0506_loop_limit.c @@ -0,0 +1,5 @@ +int x = 0; +while (rand(0,1)==0) { + if (x < 10000) x = x + 1; +} +print(x); diff --git a/tests/sources/0507_loop_limit2.c b/tests/sources/0507_loop_limit2.c new file mode 100644 index 0000000..bafdf77 --- /dev/null +++ b/tests/sources/0507_loop_limit2.c @@ -0,0 +1,6 @@ +int x = 0; +int N = rand(0,1000); +while (rand(0,1)==0) { + if (x < N) x = x + 1; +} +print(x); diff --git a/tests/sources/0508_loop_init.c b/tests/sources/0508_loop_init.c new file mode 100644 index 0000000..f0817e5 --- /dev/null +++ b/tests/sources/0508_loop_init.c @@ -0,0 +1,14 @@ +int init; +int x; + +init = 0; +while (rand(0,1)==0) { + if (init == 0) { + x = 0; + init = 1; + } + else { + x = x + 1; + } + assert(x >= 0); +} diff --git a/tests/sources/0509_loop_nested.c b/tests/sources/0509_loop_nested.c new file mode 100644 index 0000000..54d5be6 --- /dev/null +++ b/tests/sources/0509_loop_nested.c @@ -0,0 +1,9 @@ +int i=0, j=0; + +while (i < 1000) { + j = 0; + while (j < i) { + j = j + 1; + } + i = i + 1; +} diff --git a/tests/sources/0510_loop_nested2.c b/tests/sources/0510_loop_nested2.c new file mode 100644 index 0000000..90c52ec --- /dev/null +++ b/tests/sources/0510_loop_nested2.c @@ -0,0 +1,10 @@ +int i,j; + +i = 0; +while (i < 1000) { + j = 0; + while (j < i) { + j = j + 1; + } + i = i + 1; +} diff --git a/tests/sources/0600_bubble_sort.c b/tests/sources/0600_bubble_sort.c new file mode 100644 index 0000000..5cad03d --- /dev/null +++ b/tests/sources/0600_bubble_sort.c @@ -0,0 +1,32 @@ +// Example from Cousot Habwachs POPL 1978 + +// Bubble sort, where array operations are abstracted away +// to get a non-deterministic scalar program + +// expected results: +// - with polyhedra, no assertion failure (proof of absence of array overflow) +// - with intervals, assertion failure + +int B,J,T; +int N = rand(0,100000); // array size + +B = N; +while (B >= 1) { + J = 1; + T = 0; + while (J <= B-1) { + + // array bound-check + assert(1 <= J && J <= N); + assert(1 <= (J+1) && (J+1) <= N); + + // the non-deterministic test models comparing TAB[J] and TAB[J+1] + if (rand(0,1)==0) { + // where, we would exchange TAB[J] and TAB[J+1]; + T = J; + } + + J = J + 1; + } + B = T; +} diff --git a/tests/sources/0601_heap_sort.c b/tests/sources/0601_heap_sort.c new file mode 100644 index 0000000..dd12e1a --- /dev/null +++ b/tests/sources/0601_heap_sort.c @@ -0,0 +1,66 @@ +// Example from Cousot Habwachs POPL 1978 + +// Heap sort, where array operations are abstracted away +// to get a non-deterministic scalar program + +// expected results: with polyhedra, no assertion failure + +int L,R,I,J; +int N = rand(1,100000); // array size + +L = N/2 + 1; +R = N; + +if (L >= 2) { + L = L - 1; + // model the assignment "K = TAB[L]" + assert(1 <= L && L <= N); +} +else { + // model the assignments "K = TAB[R]; TAB[R] = TAB[1]" + assert(1 <= R && R <= N); + assert(1 <= 1 && 1 <= N); + R = R - 1; +} + +while (R >= 2) { + I = L; + J = 2*I; + + while (J <= R && rand(0,1)==0) { + if (J <= R-1) { + // model the comparison "TAB[J] < TAB[J+1]" + assert(1 <= J && J <= N); + assert(1 <= (J+1) && (J+1) <= N); + if (rand(0,1)==0) { J = J + 1; } + } + + // model the comparison "K < TAB[J]" + assert(1 <= J && J <= N); + if (rand(0,1)==0) { + // model the assignment "TAB[I] = TAB[J]" + assert(1 <= I && I <= N); + assert(1 <= J && J <= N); + I = J; + J = 2*J; + } + } + + // model the assignment "TAB[I] = K" + assert(1 <= I && I <= N); + + if (L >= 2) { + L = L - 1; + // model the assignment "K = TAB[L]" + assert(1 <= L && L <= N); + } + else { + // model the assignments "K = TAB[R]; TAB[R] = TAB[1]" + assert(1 <= R && R <= N); + assert(1 <= 1 && 1 <= N); + R = R - 1; + } + + // model the assignment "TAB[1] = K" + assert(1 <= 1 && 1 <= N); +} diff --git a/tests/sources/0602_rate_limiter.c b/tests/sources/0602_rate_limiter.c new file mode 100644 index 0000000..a36da77 --- /dev/null +++ b/tests/sources/0602_rate_limiter.c @@ -0,0 +1,26 @@ +// Example from Miné HOSC 2006 + +// Rate limiter: at each loop iteration, a new input is fetched (X) and +// a new output (Y) is computed; Y tries to follow X but is limited to +// change no more that a given slope (D) in absolute value + +// To prove that the assertion holds, this version needs the polyhedra +// domain and an unrolling factor of at least 6 + +int X; // input +int Y; // output +int S; // last output +int D; // maximum slope; + +Y = 0; +while (rand(0,1)==1) { + X = rand(-128,128); + D = rand(0,16); + S = Y; + int R = X - S; // current slope + Y = X; + if (R <= -D) Y = S - D; // slope too small + else if (R >= D) Y = S + D; // slope too large +} + +assert(Y >= -128 && Y <= 128); diff --git a/tests/sources/0603_rate_limiter2.c b/tests/sources/0603_rate_limiter2.c new file mode 100644 index 0000000..32a7a17 --- /dev/null +++ b/tests/sources/0603_rate_limiter2.c @@ -0,0 +1,21 @@ +// This version is similar to the previous one, but the assertion is checked +// inside the loop +// No unrolling is necessary in this version! + +int X; // input +int Y; // output +int S; // last output +int D; // maximum slope; + +Y = 0; +while (rand(0,1)==1) { + X = rand(-128,128); + D = rand(0,16); + S = Y; + int R = X - S; // current slope + Y = X; + if (R <= -D) Y = S - D; // slope too small + else if (R >= D) Y = S + D; // slope too large + + assert(Y >= -128 && Y <= 128); +} |