From c19c2495497d0dfa7aaf871cf833cd5e5f986d33 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Tue, 31 May 2016 12:59:38 -0600 Subject: moved all the tests to the testing folder --- Test/floats/test1.bpl | 13 ++++++++++++ Test/floats/test10.bpl | 20 ++++++++++++++++++ Test/floats/test11.bpl | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++ Test/floats/test12.bpl | 43 +++++++++++++++++++++++++++++++++++++++ Test/floats/test13.bpl | 19 +++++++++++++++++ Test/floats/test14.bpl | 20 ++++++++++++++++++ Test/floats/test15.bpl | 24 ++++++++++++++++++++++ Test/floats/test16.bpl | 8 ++++++++ Test/floats/test17.bpl | 11 ++++++++++ Test/floats/test18.bpl | 36 +++++++++++++++++++++++++++++++++ Test/floats/test19.bpl | 36 +++++++++++++++++++++++++++++++++ Test/floats/test2.bpl | 17 ++++++++++++++++ Test/floats/test20.bpl | 14 +++++++++++++ Test/floats/test3.bpl | 13 ++++++++++++ Test/floats/test4.bpl | 32 +++++++++++++++++++++++++++++ Test/floats/test5.bpl | 36 +++++++++++++++++++++++++++++++++ Test/floats/test6.bpl | 40 ++++++++++++++++++++++++++++++++++++ Test/floats/test7.bpl | 38 ++++++++++++++++++++++++++++++++++ Test/floats/test8.bpl | 16 +++++++++++++++ Test/floats/test9.bpl | 34 +++++++++++++++++++++++++++++++ float_test.bpl | 13 ------------ float_test10.bpl | 20 ------------------ float_test11.bpl | 55 -------------------------------------------------- float_test12.bpl | 43 --------------------------------------- float_test13.bpl | 19 ----------------- float_test14.bpl | 20 ------------------ float_test15.bpl | 24 ---------------------- float_test16.bpl | 8 -------- float_test17.bpl | 11 ---------- float_test18.bpl | 36 --------------------------------- float_test19.bpl | 36 --------------------------------- float_test2.bpl | 17 ---------------- float_test20.bpl | 14 ------------- float_test3.bpl | 13 ------------ float_test4.bpl | 32 ----------------------------- float_test5.bpl | 36 --------------------------------- float_test6.bpl | 40 ------------------------------------ float_test7.bpl | 38 ---------------------------------- float_test8.bpl | 16 --------------- float_test9.bpl | 34 ------------------------------- 40 files changed, 525 insertions(+), 525 deletions(-) create mode 100644 Test/floats/test1.bpl create mode 100644 Test/floats/test10.bpl create mode 100644 Test/floats/test11.bpl create mode 100644 Test/floats/test12.bpl create mode 100644 Test/floats/test13.bpl create mode 100644 Test/floats/test14.bpl create mode 100644 Test/floats/test15.bpl create mode 100644 Test/floats/test16.bpl create mode 100644 Test/floats/test17.bpl create mode 100644 Test/floats/test18.bpl create mode 100644 Test/floats/test19.bpl create mode 100644 Test/floats/test2.bpl create mode 100644 Test/floats/test20.bpl create mode 100644 Test/floats/test3.bpl create mode 100644 Test/floats/test4.bpl create mode 100644 Test/floats/test5.bpl create mode 100644 Test/floats/test6.bpl create mode 100644 Test/floats/test7.bpl create mode 100644 Test/floats/test8.bpl create mode 100644 Test/floats/test9.bpl delete mode 100644 float_test.bpl delete mode 100644 float_test10.bpl delete mode 100644 float_test11.bpl delete mode 100644 float_test12.bpl delete mode 100644 float_test13.bpl delete mode 100644 float_test14.bpl delete mode 100644 float_test15.bpl delete mode 100644 float_test16.bpl delete mode 100644 float_test17.bpl delete mode 100644 float_test18.bpl delete mode 100644 float_test19.bpl delete mode 100644 float_test2.bpl delete mode 100644 float_test20.bpl delete mode 100644 float_test3.bpl delete mode 100644 float_test4.bpl delete mode 100644 float_test5.bpl delete mode 100644 float_test6.bpl delete mode 100644 float_test7.bpl delete mode 100644 float_test8.bpl delete mode 100644 float_test9.bpl diff --git a/Test/floats/test1.bpl b/Test/floats/test1.bpl new file mode 100644 index 00000000..e893e098 --- /dev/null +++ b/Test/floats/test1.bpl @@ -0,0 +1,13 @@ +//Translation from addsub_double_exact.c +//Should Verify +procedure main() returns () { + var x : float<11, 53>; + var y : float<11, 53>; + var z : float<11, 53>; + var r : float<11, 53>; + x := fp<11, 53> (10000000bv64); + y := x + fp<11, 53>(1bv64); + z := x - fp<11, 53>(1bv64); + r := y - z; + assert r == fp<11, 53> (2bv64); +} \ No newline at end of file diff --git a/Test/floats/test10.bpl b/Test/floats/test10.bpl new file mode 100644 index 00000000..566f7a56 --- /dev/null +++ b/Test/floats/test10.bpl @@ -0,0 +1,20 @@ +//Translation from loop.c +//Should return an error? (The real case does as well...) + +procedure main() returns () { + var x : float; + var y : float; + var z : float; + + x := fp(1); + y := fp(10000000); + z := fp(42); + + while (x < y) { + x := x + fp(1); + y := y - fp(1); + z := z + fp(1); + } + + assert(z >= fp(0) && z <= fp(10000000)); +} \ No newline at end of file diff --git a/Test/floats/test11.bpl b/Test/floats/test11.bpl new file mode 100644 index 00000000..cee3e36e --- /dev/null +++ b/Test/floats/test11.bpl @@ -0,0 +1,55 @@ +//Translation from interpolation.c +//Should Verify +//Returns inconclusive? What does that mean? + +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); +procedure main() returns () { + var i : int; + var z : float32; + var t : float32; + var min : [int] float32; + var max : [int] float32; + + min[0] := TO_FLOAT32_INT(5); + min[1] := TO_FLOAT32_INT(10); + min[2] := TO_FLOAT32_INT(12); + min[3] := TO_FLOAT32_INT(30); + min[4] := TO_FLOAT32_INT(150); + + max[0] := TO_FLOAT32_INT(10); + max[1] := TO_FLOAT32_INT(12); + max[2] := TO_FLOAT32_INT(30); + max[3] := TO_FLOAT32_INT(150); + max[4] := TO_FLOAT32_INT(300); + + havoc t; + assume(t >= min[0] && t <= max[4]); + + i := 0; + //while (i < 5) { + //if (t <= max[i]) { + //break; + //} + //i := i + 1; + //} + + if (t > max[0]) { //1 + i := i + 1; + } + if (t > max[1]) { //2 + i := i + 1; + } + if (t > max[2]) { //3 + i := i + 1; + } + if (t > max[3]) { //4 + i := i + 1; + } + if (t > max[4]) { //5 + i := i + 1; + } + + z := (t - min[i]) / (max[i] - min[i]); + + assert(z >= TO_FLOAT32_INT(0) && z <= TO_FLOAT32_INT(1)); +} \ No newline at end of file diff --git a/Test/floats/test12.bpl b/Test/floats/test12.bpl new file mode 100644 index 00000000..c733b9f4 --- /dev/null +++ b/Test/floats/test12.bpl @@ -0,0 +1,43 @@ +//Translation from inv_Newton.c +//Should Verify +//Unfinished code! + +procedure inv(float(11 53)) returns(float(11 53)) { + var z : float(11 53); + var t : float(11 53); + var t : float(11 53); + + +} + +procedure main() returns () { + var t : float(11 53); + var t : float(11 53); + + min[0] := fp(5); + min[1] := fp(10); + min[2] := fp(12); + min[3] := fp(30); + min[4] := fp(150); + + max[0] := fp(10); + max[1] := fp(12); + max[2] := fp(30); + max[3] := fp(150); + max[4] := fp(300); + + havoc t; + assume(t >= min[0] && t <= max[4]); + + i := 0; + while (i < 5) { + if (t <= max[i]) { + break; + } + i := i + 1; + } + + z := (t - min[i]) / (max[i] - min[i]); + + assert(z >= fp(0) && z <= fp(1)); +} \ No newline at end of file diff --git a/Test/floats/test13.bpl b/Test/floats/test13.bpl new file mode 100644 index 00000000..e5402539 --- /dev/null +++ b/Test/floats/test13.bpl @@ -0,0 +1,19 @@ +//Translation from inv_square_false-unreach-call.c +//Should return an error (without crashing) + +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); + +procedure main() returns () { + var x : float32; + var y : float32; + var z : float32; + + havoc x; + assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1)); + + if (x != TO_FLOAT32_INT(0)) { + y := x * x; + assert(y != TO_FLOAT32_INT(0)); + z := TO_FLOAT32_INT(1) / y; + } +} \ No newline at end of file diff --git a/Test/floats/test14.bpl b/Test/floats/test14.bpl new file mode 100644 index 00000000..1505c361 --- /dev/null +++ b/Test/floats/test14.bpl @@ -0,0 +1,20 @@ +//Translation from inv_square_true-unreach-call.c +//Should Verify + +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32); + +procedure main() returns () { + var x : float32; + var y : float32; + var z : float32; + + havoc x; + assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1)); + + if (x <= TO_FLOAT32_REAL(-1e-20) || x >= TO_FLOAT32_REAL(1e-20)) { + y := x * x; + assert(y != TO_FLOAT32_INT(0)); + z := TO_FLOAT32_INT(1) / y; + } +} \ No newline at end of file diff --git a/Test/floats/test15.bpl b/Test/floats/test15.bpl new file mode 100644 index 00000000..1dc549ac --- /dev/null +++ b/Test/floats/test15.bpl @@ -0,0 +1,24 @@ +//Translation from Muller_Kahan.c +//Should Verify +//NOTE: (fp(....)) causes a compiler error! +//FAILS! Heavily... + +procedure main() returns () { + var x0 : float(11 53); + var x1 : float(11 53); + var x2 : float(11 53); + var i : int; + + x0 := fp(11 11 53) / fp(2 11 53); + x1 := fp(61 11 53) / fp(11 11 53); + i := 0; + while (i < 100) { + x2 := fp(1130 11 53) - fp(3000 11 53) / x0; + x2 := fp(111 11 53) - x2 / x1; + x0 := x1; + x1 := x2; + i := i + 1; + } + + assert(x0 >= fp(99 11 53) && x0 <= fp(101 11 53)); +} \ No newline at end of file diff --git a/Test/floats/test16.bpl b/Test/floats/test16.bpl new file mode 100644 index 00000000..69ae243d --- /dev/null +++ b/Test/floats/test16.bpl @@ -0,0 +1,8 @@ +//Translation from nan_double_false-unreach-call.c +//Should return an error + +procedure main() returns () { + var x : float(11 53); + havoc x; + assert(x==x); +} \ No newline at end of file diff --git a/Test/floats/test17.bpl b/Test/floats/test17.bpl new file mode 100644 index 00000000..caa1fa74 --- /dev/null +++ b/Test/floats/test17.bpl @@ -0,0 +1,11 @@ +//Translation from nan_double_range_true-unreach-call.c +//Should verify +//Uggghhhh, should I add support for e? + +procedure main() returns () { + var x : float(11 53); + havoc x; + if (x >= fp(-100000000000000000000000000 11 53) && x <= fp(100000000000000000000000000 11 53)) { + assert(x==x); + } +} \ No newline at end of file diff --git a/Test/floats/test18.bpl b/Test/floats/test18.bpl new file mode 100644 index 00000000..71eb5286 --- /dev/null +++ b/Test/floats/test18.bpl @@ -0,0 +1,36 @@ +//Translation from rlim_exit.c +//Should verify +//Unary - unsupported float operations (on my end)... + +procedure main() returns () { + var X : float; + var Y : float; + var S : float; + var R : float; + var D : float; + var i : int; + + Y := fp(0); + + i := 0; + while (i < 100000) { + havoc X; + havoc D; + assume(X >= fp(-128) && X <= fp(128)); + assume(D >= fp(0) && D <= fp(16)); + + S := Y; + Y := X; + R := X - S; + if (R <= fp(0)-D) { + Y := S - D; + } + else if(R >= D) { + Y := S + D; + } + + i := i + 1; + } + + assert(Y >= fp(-129) && Y <= fp(129)); +} \ No newline at end of file diff --git a/Test/floats/test19.bpl b/Test/floats/test19.bpl new file mode 100644 index 00000000..f00d8a2b --- /dev/null +++ b/Test/floats/test19.bpl @@ -0,0 +1,36 @@ +//Translation from flim_invariant.c +//Should verify +//Unary - unsupported float operations (on my end)... + +procedure main() returns () { + var X : float; + var Y : float; + var S : float; + var R : float; + var D : float; + var i : int; + + Y := fp(0); + + i := 0; + while (i < 100000) { + havoc X; + havoc D; + assume(X >= fp(-128) && X <= fp(128)); + assume(D >= fp(0) && D <= fp(16)); + + S := Y; + Y := X; + R := X - S; + if (R <= fp(0)-D) { + Y := S - D; + } + else if(R >= D) { + Y := S + D; + } + + assert(Y >= fp(-129) && Y <= fp(129)); + + i := i + 1; + } +} \ No newline at end of file diff --git a/Test/floats/test2.bpl b/Test/floats/test2.bpl new file mode 100644 index 00000000..d78c339d --- /dev/null +++ b/Test/floats/test2.bpl @@ -0,0 +1,17 @@ +//Translation from addsub_float_exact.c +//Should Verify + +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32); + +procedure main() returns () { + var x : float32; + var y : float32; + var z : float32; + var r : float32; + x := TO_FLOAT32_REAL(1e7); + y := x + TO_FLOAT32_INT(1); + z := x - TO_FLOAT32_INT(1); + r := y - z; + assert r == TO_FLOAT32_INT(2); +} \ No newline at end of file diff --git a/Test/floats/test20.bpl b/Test/floats/test20.bpl new file mode 100644 index 00000000..57c605fd --- /dev/null +++ b/Test/floats/test20.bpl @@ -0,0 +1,14 @@ +//Should return an error? +//Translation from Rump_double.c + +procedure main() returns () { + var x : float(11 53); + var y : float(11 53); + var r : float(11 53); + + x := fp(77617 11 53); + y := fp(33096 11 53); + r := y*y*y*y*y*y * fp(333.75 11 53) + x*x * (x*x*y*y*fp(11 11 53) - y*y*y*y*y*y - y*y*y*y * fp(121 11 53) - fp(2 11 53)) + y*y*y*y*y*y*y*y * fp(5.5 11 53) + x / (y*fp(2 11 53)); + + assert(r >= fp(0 11 53)); +} \ No newline at end of file diff --git a/Test/floats/test3.bpl b/Test/floats/test3.bpl new file mode 100644 index 00000000..67c6ba48 --- /dev/null +++ b/Test/floats/test3.bpl @@ -0,0 +1,13 @@ +//Translation from addsub_float_inexact.c +//Should give an error +procedure main() returns () { + var x : float32; + var y : float32; + var z : float32; + var r : float32; + x := fp<8, 24>(3221225472bv32); + y := x + fp<8, 24>(1bv32); + z := x - fp<8, 24>(1bv32); + r := y - z; + assert r == fp<8, 24>(2bv32); +} \ No newline at end of file diff --git a/Test/floats/test4.bpl b/Test/floats/test4.bpl new file mode 100644 index 00000000..a31aa215 --- /dev/null +++ b/Test/floats/test4.bpl @@ -0,0 +1,32 @@ +//Translation from drift_tenth.c +//Should Fail + +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32); + +procedure main() returns () { + var tick : float32; + var time : float32; + var i: int; + + tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10); + time := TO_FLOAT32_INT(0); + + //i := 0; + //while (i < 10) + //{ + // time := time + tick; + // i := i + 1; + //} + time := time + tick;//1 + time := time + tick;//2 + time := time + tick;//3 + time := time + tick;//4 + time := time + tick;//5 + time := time + tick;//6 + time := time + tick;//7 + time := time + tick;//8 + time := time + tick;//9 + time := time + tick;//10 + assert time == TO_FLOAT32_INT(1); +} \ No newline at end of file diff --git a/Test/floats/test5.bpl b/Test/floats/test5.bpl new file mode 100644 index 00000000..7536f8fd --- /dev/null +++ b/Test/floats/test5.bpl @@ -0,0 +1,36 @@ +//Translation from filter1.c +//Should Verify + +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float64); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64); + +procedure main() returns () { + var E0 : float64; + var E1 : float64; + var S : float64); + var i : int; + var rand : int; + + E1 := TO_FLOAT64_INT(0); + S := TO_FLOAT64_INT(0); + + i := 0; + while (i <= 1000000) + { + havoc E0; + assume(E0 >= fp(-1 11 53) && E0 <= fp(1 11 53)); + + havoc rand; + if (rand != 0) { + S := fp(0 11 53); + } + else { + S := fp(0.999 11 53) * S + E0 - E1; + } + E1 := E0; + + //assert(1==0); + assert(S >= fp(-1 11 53) && S <= fp(1 11 53)); + i := i + 1; + } +} \ No newline at end of file diff --git a/Test/floats/test6.bpl b/Test/floats/test6.bpl new file mode 100644 index 00000000..6bef1137 --- /dev/null +++ b/Test/floats/test6.bpl @@ -0,0 +1,40 @@ +//Translation from filter2.c +//Should give an error +//FAILS; doesn't generate terms! + +procedure main() returns () { + var E : float(11 53); + var E0 : float(11 53); + var E1 : float(11 53); + var S : float(11 53); + var S0 : float(11 53); + var S1 : float(11 53); + var i: int; + + havoc E; + havoc E0; + assume(E >= fp(0.0 11 53) && E <= fp(1.0 11 53)); + assume(E0 >= fp(0.0 11 53) && E0 <= fp(1.0 11 53)); + + E1 := fp(0.0 11 53); + S1 := fp(0.0 11 53); + S0 := fp(0.0 11 53); + S := fp(0.0 11 53); + + i := 0; +// while (i <= 1000000) +// { + E1 := E0; + E0 := E; + + havoc E; + assume(E >= fp(0.0 11 53) && E <= fp(1.0 11 53)); + + S1 := S0; + S0 := S; + S := E*fp(0.7 11 53) - E0*fp(1.3 11 53) + E1*fp(1.1 11 53) + S0*fp(1.4 11 53) - S1*fp(0.7 11 53); + + assert(S >= fp(-4.0 11 53) && S <= fp(4.0 11 53)); + //i := i + 1; +// } +} \ No newline at end of file diff --git a/Test/floats/test7.bpl b/Test/floats/test7.bpl new file mode 100644 index 00000000..8e07878d --- /dev/null +++ b/Test/floats/test7.bpl @@ -0,0 +1,38 @@ +//Translation from filter2.c +//Should give an error +//Same as the previous one; it works with reals! + +procedure main() returns () { + var E : real; + var E0 : real; + var E1 : real; + var S : real; + var S0 : real; + var S1 : real; + var i: int; + + havoc E; + havoc E0; + assume(E >= 0.0 && E <= 1.0); + assume(E0 >= 0.0 && E0 <= 1.0); + + S0 := 0.0; + S := 0.0; + + i := 0; + while (i <= 1000000) + { + E1 := E0; + E0 := E; + + havoc E; + assume(E >= 0.0 && E <= 1.0); + + S1 := S0; + S0 := S; + S := E*0.7 - E0*1.3 + E1*1.1 + S0*1.4 - S1*0.7; + + assert(S >= -4.0 && S <= 4.0); + i := i + 1; + } +} \ No newline at end of file diff --git a/Test/floats/test8.bpl b/Test/floats/test8.bpl new file mode 100644 index 00000000..7e78e206 --- /dev/null +++ b/Test/floats/test8.bpl @@ -0,0 +1,16 @@ +//Translation from float_double.c +//Should Verify + +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float32) returns (float64); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float64) returns (float32); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float64); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64); + +procedure main() returns () { + var x : float64; + var y : float32; + + x := TO_FLOAT64_REAL(1e20)+TO_FLOAT64_INT(1); + y := TO_FLOAT32_FLOAT64(x); + assert x != TO_FLOAT64_FLOAT32(y); +} \ No newline at end of file diff --git a/Test/floats/test9.bpl b/Test/floats/test9.bpl new file mode 100644 index 00000000..c3a42e6b --- /dev/null +++ b/Test/floats/test9.bpl @@ -0,0 +1,34 @@ +//Translation from feedback_diverge.c +//Should give an error +//Not sure on this one... + +procedure main() returns () { + var A : float; + var B : float; + var X : float; + var i : int; + var rand : int; + + A := fp(0); + B := fp(0); + + i := 0; + while (i < 3600000) { + + havoc rand; + if (rand != 0) { + havoc X; + assume(X >= fp(-20) && X <= fp(20)); + } + else { + X := B; + } + + B := B - (B * fp(2.0) - A - X) * fp(.005); + A := X; + + i := i + 1; + } + + assert(A >= fp(-100) && A <= fp(100)); +} \ No newline at end of file diff --git a/float_test.bpl b/float_test.bpl deleted file mode 100644 index e893e098..00000000 --- a/float_test.bpl +++ /dev/null @@ -1,13 +0,0 @@ -//Translation from addsub_double_exact.c -//Should Verify -procedure main() returns () { - var x : float<11, 53>; - var y : float<11, 53>; - var z : float<11, 53>; - var r : float<11, 53>; - x := fp<11, 53> (10000000bv64); - y := x + fp<11, 53>(1bv64); - z := x - fp<11, 53>(1bv64); - r := y - z; - assert r == fp<11, 53> (2bv64); -} \ No newline at end of file diff --git a/float_test10.bpl b/float_test10.bpl deleted file mode 100644 index 566f7a56..00000000 --- a/float_test10.bpl +++ /dev/null @@ -1,20 +0,0 @@ -//Translation from loop.c -//Should return an error? (The real case does as well...) - -procedure main() returns () { - var x : float; - var y : float; - var z : float; - - x := fp(1); - y := fp(10000000); - z := fp(42); - - while (x < y) { - x := x + fp(1); - y := y - fp(1); - z := z + fp(1); - } - - assert(z >= fp(0) && z <= fp(10000000)); -} \ No newline at end of file diff --git a/float_test11.bpl b/float_test11.bpl deleted file mode 100644 index cee3e36e..00000000 --- a/float_test11.bpl +++ /dev/null @@ -1,55 +0,0 @@ -//Translation from interpolation.c -//Should Verify -//Returns inconclusive? What does that mean? - -function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); -procedure main() returns () { - var i : int; - var z : float32; - var t : float32; - var min : [int] float32; - var max : [int] float32; - - min[0] := TO_FLOAT32_INT(5); - min[1] := TO_FLOAT32_INT(10); - min[2] := TO_FLOAT32_INT(12); - min[3] := TO_FLOAT32_INT(30); - min[4] := TO_FLOAT32_INT(150); - - max[0] := TO_FLOAT32_INT(10); - max[1] := TO_FLOAT32_INT(12); - max[2] := TO_FLOAT32_INT(30); - max[3] := TO_FLOAT32_INT(150); - max[4] := TO_FLOAT32_INT(300); - - havoc t; - assume(t >= min[0] && t <= max[4]); - - i := 0; - //while (i < 5) { - //if (t <= max[i]) { - //break; - //} - //i := i + 1; - //} - - if (t > max[0]) { //1 - i := i + 1; - } - if (t > max[1]) { //2 - i := i + 1; - } - if (t > max[2]) { //3 - i := i + 1; - } - if (t > max[3]) { //4 - i := i + 1; - } - if (t > max[4]) { //5 - i := i + 1; - } - - z := (t - min[i]) / (max[i] - min[i]); - - assert(z >= TO_FLOAT32_INT(0) && z <= TO_FLOAT32_INT(1)); -} \ No newline at end of file diff --git a/float_test12.bpl b/float_test12.bpl deleted file mode 100644 index c733b9f4..00000000 --- a/float_test12.bpl +++ /dev/null @@ -1,43 +0,0 @@ -//Translation from inv_Newton.c -//Should Verify -//Unfinished code! - -procedure inv(float(11 53)) returns(float(11 53)) { - var z : float(11 53); - var t : float(11 53); - var t : float(11 53); - - -} - -procedure main() returns () { - var t : float(11 53); - var t : float(11 53); - - min[0] := fp(5); - min[1] := fp(10); - min[2] := fp(12); - min[3] := fp(30); - min[4] := fp(150); - - max[0] := fp(10); - max[1] := fp(12); - max[2] := fp(30); - max[3] := fp(150); - max[4] := fp(300); - - havoc t; - assume(t >= min[0] && t <= max[4]); - - i := 0; - while (i < 5) { - if (t <= max[i]) { - break; - } - i := i + 1; - } - - z := (t - min[i]) / (max[i] - min[i]); - - assert(z >= fp(0) && z <= fp(1)); -} \ No newline at end of file diff --git a/float_test13.bpl b/float_test13.bpl deleted file mode 100644 index e5402539..00000000 --- a/float_test13.bpl +++ /dev/null @@ -1,19 +0,0 @@ -//Translation from inv_square_false-unreach-call.c -//Should return an error (without crashing) - -function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); - -procedure main() returns () { - var x : float32; - var y : float32; - var z : float32; - - havoc x; - assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1)); - - if (x != TO_FLOAT32_INT(0)) { - y := x * x; - assert(y != TO_FLOAT32_INT(0)); - z := TO_FLOAT32_INT(1) / y; - } -} \ No newline at end of file diff --git a/float_test14.bpl b/float_test14.bpl deleted file mode 100644 index 1505c361..00000000 --- a/float_test14.bpl +++ /dev/null @@ -1,20 +0,0 @@ -//Translation from inv_square_true-unreach-call.c -//Should Verify - -function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); -function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32); - -procedure main() returns () { - var x : float32; - var y : float32; - var z : float32; - - havoc x; - assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1)); - - if (x <= TO_FLOAT32_REAL(-1e-20) || x >= TO_FLOAT32_REAL(1e-20)) { - y := x * x; - assert(y != TO_FLOAT32_INT(0)); - z := TO_FLOAT32_INT(1) / y; - } -} \ No newline at end of file diff --git a/float_test15.bpl b/float_test15.bpl deleted file mode 100644 index 1dc549ac..00000000 --- a/float_test15.bpl +++ /dev/null @@ -1,24 +0,0 @@ -//Translation from Muller_Kahan.c -//Should Verify -//NOTE: (fp(....)) causes a compiler error! -//FAILS! Heavily... - -procedure main() returns () { - var x0 : float(11 53); - var x1 : float(11 53); - var x2 : float(11 53); - var i : int; - - x0 := fp(11 11 53) / fp(2 11 53); - x1 := fp(61 11 53) / fp(11 11 53); - i := 0; - while (i < 100) { - x2 := fp(1130 11 53) - fp(3000 11 53) / x0; - x2 := fp(111 11 53) - x2 / x1; - x0 := x1; - x1 := x2; - i := i + 1; - } - - assert(x0 >= fp(99 11 53) && x0 <= fp(101 11 53)); -} \ No newline at end of file diff --git a/float_test16.bpl b/float_test16.bpl deleted file mode 100644 index 69ae243d..00000000 --- a/float_test16.bpl +++ /dev/null @@ -1,8 +0,0 @@ -//Translation from nan_double_false-unreach-call.c -//Should return an error - -procedure main() returns () { - var x : float(11 53); - havoc x; - assert(x==x); -} \ No newline at end of file diff --git a/float_test17.bpl b/float_test17.bpl deleted file mode 100644 index caa1fa74..00000000 --- a/float_test17.bpl +++ /dev/null @@ -1,11 +0,0 @@ -//Translation from nan_double_range_true-unreach-call.c -//Should verify -//Uggghhhh, should I add support for e? - -procedure main() returns () { - var x : float(11 53); - havoc x; - if (x >= fp(-100000000000000000000000000 11 53) && x <= fp(100000000000000000000000000 11 53)) { - assert(x==x); - } -} \ No newline at end of file diff --git a/float_test18.bpl b/float_test18.bpl deleted file mode 100644 index 71eb5286..00000000 --- a/float_test18.bpl +++ /dev/null @@ -1,36 +0,0 @@ -//Translation from rlim_exit.c -//Should verify -//Unary - unsupported float operations (on my end)... - -procedure main() returns () { - var X : float; - var Y : float; - var S : float; - var R : float; - var D : float; - var i : int; - - Y := fp(0); - - i := 0; - while (i < 100000) { - havoc X; - havoc D; - assume(X >= fp(-128) && X <= fp(128)); - assume(D >= fp(0) && D <= fp(16)); - - S := Y; - Y := X; - R := X - S; - if (R <= fp(0)-D) { - Y := S - D; - } - else if(R >= D) { - Y := S + D; - } - - i := i + 1; - } - - assert(Y >= fp(-129) && Y <= fp(129)); -} \ No newline at end of file diff --git a/float_test19.bpl b/float_test19.bpl deleted file mode 100644 index f00d8a2b..00000000 --- a/float_test19.bpl +++ /dev/null @@ -1,36 +0,0 @@ -//Translation from flim_invariant.c -//Should verify -//Unary - unsupported float operations (on my end)... - -procedure main() returns () { - var X : float; - var Y : float; - var S : float; - var R : float; - var D : float; - var i : int; - - Y := fp(0); - - i := 0; - while (i < 100000) { - havoc X; - havoc D; - assume(X >= fp(-128) && X <= fp(128)); - assume(D >= fp(0) && D <= fp(16)); - - S := Y; - Y := X; - R := X - S; - if (R <= fp(0)-D) { - Y := S - D; - } - else if(R >= D) { - Y := S + D; - } - - assert(Y >= fp(-129) && Y <= fp(129)); - - i := i + 1; - } -} \ No newline at end of file diff --git a/float_test2.bpl b/float_test2.bpl deleted file mode 100644 index d78c339d..00000000 --- a/float_test2.bpl +++ /dev/null @@ -1,17 +0,0 @@ -//Translation from addsub_float_exact.c -//Should Verify - -function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); -function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32); - -procedure main() returns () { - var x : float32; - var y : float32; - var z : float32; - var r : float32; - x := TO_FLOAT32_REAL(1e7); - y := x + TO_FLOAT32_INT(1); - z := x - TO_FLOAT32_INT(1); - r := y - z; - assert r == TO_FLOAT32_INT(2); -} \ No newline at end of file diff --git a/float_test20.bpl b/float_test20.bpl deleted file mode 100644 index 57c605fd..00000000 --- a/float_test20.bpl +++ /dev/null @@ -1,14 +0,0 @@ -//Should return an error? -//Translation from Rump_double.c - -procedure main() returns () { - var x : float(11 53); - var y : float(11 53); - var r : float(11 53); - - x := fp(77617 11 53); - y := fp(33096 11 53); - r := y*y*y*y*y*y * fp(333.75 11 53) + x*x * (x*x*y*y*fp(11 11 53) - y*y*y*y*y*y - y*y*y*y * fp(121 11 53) - fp(2 11 53)) + y*y*y*y*y*y*y*y * fp(5.5 11 53) + x / (y*fp(2 11 53)); - - assert(r >= fp(0 11 53)); -} \ No newline at end of file diff --git a/float_test3.bpl b/float_test3.bpl deleted file mode 100644 index 67c6ba48..00000000 --- a/float_test3.bpl +++ /dev/null @@ -1,13 +0,0 @@ -//Translation from addsub_float_inexact.c -//Should give an error -procedure main() returns () { - var x : float32; - var y : float32; - var z : float32; - var r : float32; - x := fp<8, 24>(3221225472bv32); - y := x + fp<8, 24>(1bv32); - z := x - fp<8, 24>(1bv32); - r := y - z; - assert r == fp<8, 24>(2bv32); -} \ No newline at end of file diff --git a/float_test4.bpl b/float_test4.bpl deleted file mode 100644 index a31aa215..00000000 --- a/float_test4.bpl +++ /dev/null @@ -1,32 +0,0 @@ -//Translation from drift_tenth.c -//Should Fail - -function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); -function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32); - -procedure main() returns () { - var tick : float32; - var time : float32; - var i: int; - - tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10); - time := TO_FLOAT32_INT(0); - - //i := 0; - //while (i < 10) - //{ - // time := time + tick; - // i := i + 1; - //} - time := time + tick;//1 - time := time + tick;//2 - time := time + tick;//3 - time := time + tick;//4 - time := time + tick;//5 - time := time + tick;//6 - time := time + tick;//7 - time := time + tick;//8 - time := time + tick;//9 - time := time + tick;//10 - assert time == TO_FLOAT32_INT(1); -} \ No newline at end of file diff --git a/float_test5.bpl b/float_test5.bpl deleted file mode 100644 index 7536f8fd..00000000 --- a/float_test5.bpl +++ /dev/null @@ -1,36 +0,0 @@ -//Translation from filter1.c -//Should Verify - -function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float64); -function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64); - -procedure main() returns () { - var E0 : float64; - var E1 : float64; - var S : float64); - var i : int; - var rand : int; - - E1 := TO_FLOAT64_INT(0); - S := TO_FLOAT64_INT(0); - - i := 0; - while (i <= 1000000) - { - havoc E0; - assume(E0 >= fp(-1 11 53) && E0 <= fp(1 11 53)); - - havoc rand; - if (rand != 0) { - S := fp(0 11 53); - } - else { - S := fp(0.999 11 53) * S + E0 - E1; - } - E1 := E0; - - //assert(1==0); - assert(S >= fp(-1 11 53) && S <= fp(1 11 53)); - i := i + 1; - } -} \ No newline at end of file diff --git a/float_test6.bpl b/float_test6.bpl deleted file mode 100644 index 6bef1137..00000000 --- a/float_test6.bpl +++ /dev/null @@ -1,40 +0,0 @@ -//Translation from filter2.c -//Should give an error -//FAILS; doesn't generate terms! - -procedure main() returns () { - var E : float(11 53); - var E0 : float(11 53); - var E1 : float(11 53); - var S : float(11 53); - var S0 : float(11 53); - var S1 : float(11 53); - var i: int; - - havoc E; - havoc E0; - assume(E >= fp(0.0 11 53) && E <= fp(1.0 11 53)); - assume(E0 >= fp(0.0 11 53) && E0 <= fp(1.0 11 53)); - - E1 := fp(0.0 11 53); - S1 := fp(0.0 11 53); - S0 := fp(0.0 11 53); - S := fp(0.0 11 53); - - i := 0; -// while (i <= 1000000) -// { - E1 := E0; - E0 := E; - - havoc E; - assume(E >= fp(0.0 11 53) && E <= fp(1.0 11 53)); - - S1 := S0; - S0 := S; - S := E*fp(0.7 11 53) - E0*fp(1.3 11 53) + E1*fp(1.1 11 53) + S0*fp(1.4 11 53) - S1*fp(0.7 11 53); - - assert(S >= fp(-4.0 11 53) && S <= fp(4.0 11 53)); - //i := i + 1; -// } -} \ No newline at end of file diff --git a/float_test7.bpl b/float_test7.bpl deleted file mode 100644 index 8e07878d..00000000 --- a/float_test7.bpl +++ /dev/null @@ -1,38 +0,0 @@ -//Translation from filter2.c -//Should give an error -//Same as the previous one; it works with reals! - -procedure main() returns () { - var E : real; - var E0 : real; - var E1 : real; - var S : real; - var S0 : real; - var S1 : real; - var i: int; - - havoc E; - havoc E0; - assume(E >= 0.0 && E <= 1.0); - assume(E0 >= 0.0 && E0 <= 1.0); - - S0 := 0.0; - S := 0.0; - - i := 0; - while (i <= 1000000) - { - E1 := E0; - E0 := E; - - havoc E; - assume(E >= 0.0 && E <= 1.0); - - S1 := S0; - S0 := S; - S := E*0.7 - E0*1.3 + E1*1.1 + S0*1.4 - S1*0.7; - - assert(S >= -4.0 && S <= 4.0); - i := i + 1; - } -} \ No newline at end of file diff --git a/float_test8.bpl b/float_test8.bpl deleted file mode 100644 index 7e78e206..00000000 --- a/float_test8.bpl +++ /dev/null @@ -1,16 +0,0 @@ -//Translation from float_double.c -//Should Verify - -function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float32) returns (float64); -function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float64) returns (float32); -function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float64); -function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64); - -procedure main() returns () { - var x : float64; - var y : float32; - - x := TO_FLOAT64_REAL(1e20)+TO_FLOAT64_INT(1); - y := TO_FLOAT32_FLOAT64(x); - assert x != TO_FLOAT64_FLOAT32(y); -} \ No newline at end of file diff --git a/float_test9.bpl b/float_test9.bpl deleted file mode 100644 index c3a42e6b..00000000 --- a/float_test9.bpl +++ /dev/null @@ -1,34 +0,0 @@ -//Translation from feedback_diverge.c -//Should give an error -//Not sure on this one... - -procedure main() returns () { - var A : float; - var B : float; - var X : float; - var i : int; - var rand : int; - - A := fp(0); - B := fp(0); - - i := 0; - while (i < 3600000) { - - havoc rand; - if (rand != 0) { - havoc X; - assume(X >= fp(-20) && X <= fp(20)); - } - else { - X := B; - } - - B := B - (B * fp(2.0) - A - X) * fp(.005); - A := X; - - i := i + 1; - } - - assert(A >= fp(-100) && A <= fp(100)); -} \ No newline at end of file -- cgit v1.2.3