From ce9d174eba6a4efd321e78fed4a6e00aab1fda2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Fri, 22 Jul 2016 15:42:33 -0600 Subject: fixed the syntax on former tests and added two fp constant translation tests --- Test/floats/float1.bpl | 10 +++++----- Test/floats/float13.bpl | 30 ++++++++++++++++++++++++++++++ Test/floats/float13.bpl.expect | 2 ++ Test/floats/float14.bpl | 22 ++++++++++++++++++++++ Test/floats/float14.bpl.expect | 9 +++++++++ Test/floats/float3.bpl | 18 +++++++++--------- Test/floats/float4.bpl | 10 +++++++++- Test/floats/float7.bpl | 8 ++++---- Test/floats/float8.bpl | 8 ++++---- 9 files changed, 94 insertions(+), 23 deletions(-) create mode 100644 Test/floats/float13.bpl create mode 100644 Test/floats/float13.bpl.expect create mode 100644 Test/floats/float14.bpl create mode 100644 Test/floats/float14.bpl.expect diff --git a/Test/floats/float1.bpl b/Test/floats/float1.bpl index 2b901c94..d7fc7837 100644 --- a/Test/floats/float1.bpl +++ b/Test/floats/float1.bpl @@ -2,12 +2,12 @@ // RUN: %diff "%s.expect" "%t" procedure foo(x : float24e8) returns (r : float24e8) { - r := 0e1f24e8; - r := 1e0f24e8; + r := 0e128f24e8; + r := 1e127f24e8; r := x; - r := x + 1e0f24e8; - r := 0e0f24e8 + 0e0f24e8; - assert(r == 0e1f24e8); + r := x + 1e127f24e8; + r := 0e127f24e8 + 0e127f24e8; + assert(r == 0e128f24e8); return; } \ No newline at end of file diff --git a/Test/floats/float13.bpl b/Test/floats/float13.bpl new file mode 100644 index 00000000..9b9fa7cb --- /dev/null +++ b/Test/floats/float13.bpl @@ -0,0 +1,30 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float24e8); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float24e8); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float53e11); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float53e11); + +procedure main() returns () { + var f : float24e8; + var fc : float24e8; + var d : float53e11; + var dc : float53e11; + + f := 2097152e129f24e8; + fc := TO_FLOAT32_INT(5); + assert(f == fc); + + f := 1048576e128f24e8; + fc := TO_FLOAT32_REAL(2.25); + assert(f == fc); + + d := 1125899906842624e1025f53e11; + dc := TO_FLOAT64_INT(5); + assert(d == dc); + + d := 562949953421312e1024f53e11; + dc := TO_FLOAT64_REAL(2.25); + //assert(d == dc); +} \ No newline at end of file diff --git a/Test/floats/float13.bpl.expect b/Test/floats/float13.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float13.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float14.bpl b/Test/floats/float14.bpl new file mode 100644 index 00000000..1752ef0d --- /dev/null +++ b/Test/floats/float14.bpl @@ -0,0 +1,22 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() returns () { + var f : float24e8; + var d : float53e11; + + f := 0e-1f24e8; //Error + f := 0e256f24e8; //Error + f := 0e255f24e8; //No Error + + f := 8388608e0f24e8; //Error + f := -8388608e0f24e8; //Error + f := 8388607e0f24e8; //No Error + + d := 0e-1f53e11; //Error + d := 0e2048f53e11; //Error + d := 0e2047f53e11; //No Error + + d := 4503599627370496e0f53e11; //Error + d := -4503599627370496e0f53e11; //Error + d := 4503599627370495e0f53e11; //No Error +} \ No newline at end of file diff --git a/Test/floats/float14.bpl.expect b/Test/floats/float14.bpl.expect new file mode 100644 index 00000000..f42b0286 --- /dev/null +++ b/Test/floats/float14.bpl.expect @@ -0,0 +1,9 @@ +float14.bpl(7,7): error: incorrectly formatted floating point, The given exponent -1 cannot fit in the bit size 8 +float14.bpl(8,7): error: incorrectly formatted floating point, The given exponent 256 cannot fit in the bit size 8 +float14.bpl(11,7): error: incorrectly formatted floating point, The given significand 8388608 cannot fit in the bit size 24 +float14.bpl(12,7): error: incorrectly formatted floating point, The given significand 8388608 cannot fit in the bit size 24 +float14.bpl(15,7): error: incorrectly formatted floating point, The given exponent -1 cannot fit in the bit size 11 +float14.bpl(16,7): error: incorrectly formatted floating point, The given exponent 2048 cannot fit in the bit size 11 +float14.bpl(19,7): error: incorrectly formatted floating point, The given significand 4503599627370496 cannot fit in the bit size 53 +float14.bpl(20,7): error: incorrectly formatted floating point, The given significand 4503599627370496 cannot fit in the bit size 53 +8 parse errors detected in float14.bpl diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl index e4de8b3b..507c4127 100644 --- a/Test/floats/float3.bpl +++ b/Test/floats/float3.bpl @@ -8,20 +8,20 @@ procedure main() returns () { z := x + y; z := x - y; z := x * y; - assume(y != 0e-127f24e8); + assume(y != 0e0f24e8); z := x / y; - z := (0e0f24e8 + 0e0f24e8 + 0e-127f24e8); - assert(z == 0e1f24e8); + z := (0e127f24e8 + 0e127f24e8 + 0e0f24e8); + assert(z == 0e128f24e8); - z := 0e1f24e8 - 0e0f24e8; - assert(z == 0e0f24e8); + z := 0e128f24e8 - 0e127f24e8; + assert(z == 0e127f24e8); - z := 0e0f24e8 * 0e0f24e8; - assert(z == 0e0f24e8); + z := 0e127f24e8 * 0e127f24e8; + assert(z == 0e127f24e8); - z := 0e0f24e8 / 0e0f24e8; - assert(z == 0e0f24e8); + z := 0e127f24e8 / 0e127f24e8; + assert(z == 0e127f24e8); return; } \ No newline at end of file diff --git a/Test/floats/float4.bpl b/Test/floats/float4.bpl index 816d8446..1c2df42e 100644 --- a/Test/floats/float4.bpl +++ b/Test/floats/float4.bpl @@ -1,11 +1,19 @@ // RUN: %boogie -proverWarnings:1 "%s" > "%t" // RUN: %diff "%s.expect" "%t" procedure foo() returns (r : float8e24) { + var d : float53e11; + r := 0NaN8e24; r := 0nan8e24; r := 0+oo8e24; r := 0-oo8e24; - r := -5e-3f8e24; + r := -5e255f8e24; + + d := 0NaN53e11; + d := 0nan53e11; + d := 0+oo53e11; + d := 0-oo53e11; + d := -200e2000f53e11; return; } \ No newline at end of file diff --git a/Test/floats/float7.bpl b/Test/floats/float7.bpl index c4951681..39fca79e 100644 --- a/Test/floats/float7.bpl +++ b/Test/floats/float7.bpl @@ -5,9 +5,9 @@ procedure main() returns () { var y : float53e11; var z : float53e11; var r : float53e11; - x := 0e40f53e11; - y := x + 0e0f53e11; - z := x - 0e0f53e11; + x := 0e1063f53e11; + y := x + 0e1023f53e11; + z := x - 0e1023f53e11; r := y - z; - assert r == 0e1f53e11; + assert r == 0e1024f53e11; } \ No newline at end of file diff --git a/Test/floats/float8.bpl b/Test/floats/float8.bpl index 25c08e4d..bfb3b9e9 100644 --- a/Test/floats/float8.bpl +++ b/Test/floats/float8.bpl @@ -5,9 +5,9 @@ procedure main() returns () { var y : float24e8; var z : float24e8; var r : float24e8; - x := 0e40f24e8; - y := x + 0e0f24e8; - z := x - 0e0f24e8; + x := 0e167f24e8; + y := x + 0e127f24e8; + z := x - 0e127f24e8; r := y - z; - assert r == 0e1f24e8; + assert r == 0e128f24e8; } \ No newline at end of file -- cgit v1.2.3