From 754f7d3ef36e11740a40a2d687f3b15195f63d9a Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 21:11:23 -0600 Subject: Polished up the floats test folder. Preparing to rebase --- Test/floats/float11.bpl.expect | 8 ++++---- Test/floats/float13.bpl | 23 ----------------------- Test/floats/float14.bpl | 17 ----------------- Test/floats/float15.bpl | 36 ------------------------------------ Test/floats/float16.bpl | 40 ---------------------------------------- Test/floats/float17.bpl | 38 -------------------------------------- Test/floats/float18.bpl | 16 ---------------- Test/floats/float19.bpl | 34 ---------------------------------- Test/floats/float20.bpl | 14 -------------- Test/floats/float21.bpl | 35 ----------------------------------- Test/floats/float22.bpl | 20 -------------------- Test/floats/float23.bpl | 8 -------- Test/floats/modpath.py | 13 ------------- 13 files changed, 4 insertions(+), 298 deletions(-) delete mode 100644 Test/floats/float13.bpl delete mode 100644 Test/floats/float14.bpl delete mode 100644 Test/floats/float15.bpl delete mode 100644 Test/floats/float16.bpl delete mode 100644 Test/floats/float17.bpl delete mode 100644 Test/floats/float18.bpl delete mode 100644 Test/floats/float19.bpl delete mode 100644 Test/floats/float20.bpl delete mode 100644 Test/floats/float21.bpl delete mode 100644 Test/floats/float22.bpl delete mode 100644 Test/floats/float23.bpl delete mode 100644 Test/floats/modpath.py diff --git a/Test/floats/float11.bpl.expect b/Test/floats/float11.bpl.expect index 19e55fef..9365da58 100644 --- a/Test/floats/float11.bpl.expect +++ b/Test/floats/float11.bpl.expect @@ -1,7 +1,7 @@ -..\Test\floats\float11.bpl(21,2): Error BP5001: This assertion might not hold. +float11.bpl(21,2): Error BP5001: This assertion might not hold. Execution trace: - ..\Test\floats\float11.bpl(12,7): anon0 - ..\Test\floats\float11.bpl(16,2): anon3_LoopHead - ..\Test\floats\float11.bpl(16,2): anon3_LoopDone + float11.bpl(12,7): anon0 + float11.bpl(16,2): anon3_LoopHead + float11.bpl(16,2): anon3_LoopDone Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/floats/float13.bpl b/Test/floats/float13.bpl deleted file mode 100644 index 4fe25140..00000000 --- a/Test/floats/float13.bpl +++ /dev/null @@ -1,23 +0,0 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -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 : float64; - - havoc x; - assume(x >= TO_FLOAT64_INT(0) && x <= TO_FLOAT64_INT(10)); - - y := x*x - x; - if (y >= TO_FLOAT64_INT(0)) { - y := x / TO_FLOAT64_INT(10); - } - else { - y := x*x + TO_FLOAT64_INT(2); - } - - assert(y >= TO_FLOAT64_INT(0) && y <= TO_FLOAT64_INT(105)); -} \ No newline at end of file diff --git a/Test/floats/float14.bpl b/Test/floats/float14.bpl deleted file mode 100644 index 46c1b07d..00000000 --- a/Test/floats/float14.bpl +++ /dev/null @@ -1,17 +0,0 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -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 : float64; - var r : float64; - - x := TO_FLOAT64_INT(77617); - y := TO_FLOAT64_INT(33096); - r := y*y*y*y*y*y * TO_FLOAT64_REAL(333.75) + x*x * (x*x*y*y*TO_FLOAT64_INT(11) - y*y*y*y*y*y - y*y*y*y * TO_FLOAT64_INT(121) - TO_FLOAT64_INT(2)) + y*y*y*y*y*y*y*y * TO_FLOAT64_REAL(5.5) + x / (y*TO_FLOAT64_INT(2)); - - assert(r >= TO_FLOAT64_INT(0)); -} \ No newline at end of file diff --git a/Test/floats/float15.bpl b/Test/floats/float15.bpl deleted file mode 100644 index 7536f8fd..00000000 --- a/Test/floats/float15.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/Test/floats/float16.bpl b/Test/floats/float16.bpl deleted file mode 100644 index 6bef1137..00000000 --- a/Test/floats/float16.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/Test/floats/float17.bpl b/Test/floats/float17.bpl deleted file mode 100644 index 8e07878d..00000000 --- a/Test/floats/float17.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/Test/floats/float18.bpl b/Test/floats/float18.bpl deleted file mode 100644 index 7e78e206..00000000 --- a/Test/floats/float18.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/Test/floats/float19.bpl b/Test/floats/float19.bpl deleted file mode 100644 index c3a42e6b..00000000 --- a/Test/floats/float19.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 diff --git a/Test/floats/float20.bpl b/Test/floats/float20.bpl deleted file mode 100644 index 57c605fd..00000000 --- a/Test/floats/float20.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/Test/floats/float21.bpl b/Test/floats/float21.bpl deleted file mode 100644 index 5fad5859..00000000 --- a/Test/floats/float21.bpl +++ /dev/null @@ -1,35 +0,0 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -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_INT(0)) { - y := x * x; - assert(y != TO_FLOAT32_INT(0)); - z := TO_FLOAT32_INT(1) / y; - } -} - -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/float22.bpl b/Test/floats/float22.bpl deleted file mode 100644 index 1505c361..00000000 --- a/Test/floats/float22.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/Test/floats/float23.bpl b/Test/floats/float23.bpl deleted file mode 100644 index 69ae243d..00000000 --- a/Test/floats/float23.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/Test/floats/modpath.py b/Test/floats/modpath.py deleted file mode 100644 index 90707701..00000000 --- a/Test/floats/modpath.py +++ /dev/null @@ -1,13 +0,0 @@ -import sys - -f = open(sys.argv[1], 'r') -to_write = "" - -for i in f: - to_write += i.replace("..\\Test\\floats\\", "") - -f.close() - -f = open(sys.argv[1], 'w') - -f.write(to_write) \ No newline at end of file -- cgit v1.2.3