diff options
author | RustanLeino <leino@microsoft.com> | 2016-08-17 13:40:57 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-08-17 13:40:57 -0700 |
commit | 12d1543333babd202d76e259418dd03c0c7c56c3 (patch) | |
tree | 69bd181ccb97621378ab630a1357bd5583cc96a8 /Test | |
parent | 529b1bc37b6da3f40dc85aef4cf252e9c98dd566 (diff) | |
parent | 2b64144fb02b68d00188ee81c27afa5fbc026b5b (diff) |
Merge pull request #35 from Checkmate50/master
Floating Point Support
Diffstat (limited to 'Test')
30 files changed, 359 insertions, 0 deletions
diff --git a/Test/floats/float0.bpl b/Test/floats/float0.bpl new file mode 100644 index 00000000..d7faa4b0 --- /dev/null +++ b/Test/floats/float0.bpl @@ -0,0 +1,14 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(x : real) returns (r : float8e24) +{ + r := 15; // Error + r := 15.0; // Error + r := 0e1f22e8; // Error + r := 1e0f23e8; // Error + r := x; // Error + r := 1e0f23e8 + 1e0f23e8; // Error + r := 1e0f24e8 + 1e0f23e8; // Error + + return; +}
\ No newline at end of file diff --git a/Test/floats/float0.bpl.expect b/Test/floats/float0.bpl.expect new file mode 100644 index 00000000..f657a846 --- /dev/null +++ b/Test/floats/float0.bpl.expect @@ -0,0 +1,8 @@ +float0.bpl(5,1): Error: mismatched types in assignment command (cannot assign int to float8e24) +float0.bpl(6,1): Error: mismatched types in assignment command (cannot assign real to float8e24) +float0.bpl(7,1): Error: mismatched types in assignment command (cannot assign float22e8 to float8e24) +float0.bpl(8,1): Error: mismatched types in assignment command (cannot assign float23e8 to float8e24) +float0.bpl(9,1): Error: mismatched types in assignment command (cannot assign real to float8e24) +float0.bpl(10,1): Error: mismatched types in assignment command (cannot assign float23e8 to float8e24) +float0.bpl(11,15): Error: invalid argument types (float24e8 and float23e8) to binary operator + +7 type checking errors detected in float0.bpl diff --git a/Test/floats/float1.bpl b/Test/floats/float1.bpl new file mode 100644 index 00000000..d7fc7837 --- /dev/null +++ b/Test/floats/float1.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(x : float24e8) returns (r : float24e8) +{ + r := 0e128f24e8; + r := 1e127f24e8; + r := x; + r := x + 1e127f24e8; + r := 0e127f24e8 + 0e127f24e8; + assert(r == 0e128f24e8); + + return; +}
\ No newline at end of file diff --git a/Test/floats/float1.bpl.expect b/Test/floats/float1.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float1.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float10.bpl b/Test/floats/float10.bpl new file mode 100644 index 00000000..ec9b4895 --- /dev/null +++ b/Test/floats/float10.bpl @@ -0,0 +1,18 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float53e11); + +procedure double_range_true() returns () { + var x : float53e11; + havoc x; + if (x >= TO_FLOAT64_REAL(-1e307) && x <= TO_FLOAT64_REAL(1e307)) { + assert(x==x); + } +} + +procedure double_range_false() returns () { + var x : float53e11; + havoc x; + assert(x==x); +}
\ No newline at end of file diff --git a/Test/floats/float10.bpl.expect b/Test/floats/float10.bpl.expect new file mode 100644 index 00000000..cae8d781 --- /dev/null +++ b/Test/floats/float10.bpl.expect @@ -0,0 +1,5 @@ +float10.bpl(17,2): Error BP5001: This assertion might not hold.
+Execution trace:
+ float10.bpl(16,2): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/floats/float11.bpl b/Test/floats/float11.bpl new file mode 100644 index 00000000..de148424 --- /dev/null +++ b/Test/floats/float11.bpl @@ -0,0 +1,22 @@ +// 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); + +procedure main() returns () { + var tick : float24e8; + var time : float24e8; + 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; + } + assert time == TO_FLOAT32_INT(1); +}
\ No newline at end of file diff --git a/Test/floats/float11.bpl.expect b/Test/floats/float11.bpl.expect new file mode 100644 index 00000000..9365da58 --- /dev/null +++ b/Test/floats/float11.bpl.expect @@ -0,0 +1,7 @@ +float11.bpl(21,2): Error BP5001: This assertion might not hold.
+Execution trace:
+ 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/float12.bpl b/Test/floats/float12.bpl new file mode 100644 index 00000000..914286bb --- /dev/null +++ b/Test/floats/float12.bpl @@ -0,0 +1,16 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float24e8) returns (float53e11); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float53e11) 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 x : float53e11; + var y : float24e8; + + 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/float12.bpl.expect b/Test/floats/float12.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float12.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float13.bpl b/Test/floats/float13.bpl new file mode 100644 index 00000000..9c99a30b --- /dev/null +++ b/Test/floats/float13.bpl @@ -0,0 +1,34 @@ +// 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 := -0e126f24e8; + fc := TO_FLOAT32_REAL(-0.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/float2.bpl b/Test/floats/float2.bpl new file mode 100644 index 00000000..ed9e60f0 --- /dev/null +++ b/Test/floats/float2.bpl @@ -0,0 +1,15 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(x : float11e5) returns(r : float24e8) { + var y : float53e11; + var z : float113e15; + + r := x; // Error + r := y; // Error + r := z; // Error + y := x; // Error + y := z; // Error + z := x; // Error + + return; +}
\ No newline at end of file diff --git a/Test/floats/float2.bpl.expect b/Test/floats/float2.bpl.expect new file mode 100644 index 00000000..3132c514 --- /dev/null +++ b/Test/floats/float2.bpl.expect @@ -0,0 +1,7 @@ +float2.bpl(7,1): Error: mismatched types in assignment command (cannot assign float11e5 to float24e8) +float2.bpl(8,1): Error: mismatched types in assignment command (cannot assign float53e11 to float24e8) +float2.bpl(9,1): Error: mismatched types in assignment command (cannot assign float113e15 to float24e8) +float2.bpl(10,1): Error: mismatched types in assignment command (cannot assign float11e5 to float53e11) +float2.bpl(11,1): Error: mismatched types in assignment command (cannot assign float113e15 to float53e11) +float2.bpl(12,1): Error: mismatched types in assignment command (cannot assign float11e5 to float113e15) +6 type checking errors detected in float2.bpl diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl new file mode 100644 index 00000000..507c4127 --- /dev/null +++ b/Test/floats/float3.bpl @@ -0,0 +1,27 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() returns () { + var x : float24e8; + var y : float24e8; + var z : float24e8; + + z := x + y; + z := x - y; + z := x * y; + assume(y != 0e0f24e8); + z := x / y; + + z := (0e127f24e8 + 0e127f24e8 + 0e0f24e8); + assert(z == 0e128f24e8); + + z := 0e128f24e8 - 0e127f24e8; + assert(z == 0e127f24e8); + + z := 0e127f24e8 * 0e127f24e8; + assert(z == 0e127f24e8); + + z := 0e127f24e8 / 0e127f24e8; + assert(z == 0e127f24e8); + + return; +}
\ No newline at end of file diff --git a/Test/floats/float3.bpl.expect b/Test/floats/float3.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float3.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float4.bpl b/Test/floats/float4.bpl new file mode 100644 index 00000000..1c2df42e --- /dev/null +++ b/Test/floats/float4.bpl @@ -0,0 +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 := -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/float4.bpl.expect b/Test/floats/float4.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float4.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float5.bpl b/Test/floats/float5.bpl new file mode 100644 index 00000000..12b19cf5 --- /dev/null +++ b/Test/floats/float5.bpl @@ -0,0 +1,23 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_INT(int) returns (float23e8); +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_REAL(real) returns (float23e8); +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV31(bv31) returns (float23e8); +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV32(bv32) returns (float23e8); +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_FLOAT824(float24e8) returns (float24e8); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_FLOAT823(float23e8) returns (float24e8); + +procedure foo(x : float24e8) returns (r : float24e8) { + r := TO_FLOAT823_INT(5); // Error + r := TO_FLOAT823_REAL(5.0); // Error + r := TO_FLOAT823_BV31(0bv31); // Error + r := TO_FLOAT823_BV32(0bv32); // Error + r := TO_FLOAT823_FLOAT824(0e0f24e8); // Error + r := TO_FLOAT824_FLOAT823(0e0f23e8); // Error + + r := TO_FLOAT823_FLOAT824(x); // Error + r := TO_FLOAT824_FLOAT823(x); // Error + + return; +}
\ No newline at end of file diff --git a/Test/floats/float5.bpl.expect b/Test/floats/float5.bpl.expect new file mode 100644 index 00000000..74649769 --- /dev/null +++ b/Test/floats/float5.bpl.expect @@ -0,0 +1,6 @@ +float5.bpl(12,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8) +float5.bpl(13,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8) +float5.bpl(14,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8) +float5.bpl(15,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8) +float5.bpl(20,27): Error: invalid type for argument 0 in application of TO_FLOAT824_FLOAT823: float24e8 (expected: float23e8) +5 type checking errors detected in float5.bpl diff --git a/Test/floats/float6.bpl b/Test/floats/float6.bpl new file mode 100644 index 00000000..fecf0385 --- /dev/null +++ b/Test/floats/float6.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 8 24) RNE"} TO_FLOAT32_BV32(bv32) returns (float24e8); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_BV64(bv64) returns (float53e11); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float53e11) returns (float24e8); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float24e8) returns (float53e11); + +procedure main() returns () { + var i : int; + var r : real; + var f32 : float24e8; + var f64 : float53e11; + + f32 := TO_FLOAT32_INT(5); + f32 := TO_FLOAT32_REAL(5.0); + + f32 := TO_FLOAT32_BV32(0bv32); + f64 := TO_FLOAT64_BV64(0bv64); + + f32 := TO_FLOAT32_FLOAT64(0e0f53e11); + f64 := TO_FLOAT64_FLOAT32(0e0f24e8); + + f32 := TO_FLOAT32_FLOAT64(f64); + f64 := TO_FLOAT64_FLOAT32(f32); + + return; +}
\ No newline at end of file diff --git a/Test/floats/float6.bpl.expect b/Test/floats/float6.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/floats/float6.bpl.expect @@ -0,0 +1,2 @@ +
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/floats/float7.bpl b/Test/floats/float7.bpl new file mode 100644 index 00000000..39fca79e --- /dev/null +++ b/Test/floats/float7.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() returns () { + var x : float53e11; + var y : float53e11; + var z : float53e11; + var r : float53e11; + x := 0e1063f53e11; + y := x + 0e1023f53e11; + z := x - 0e1023f53e11; + r := y - z; + assert r == 0e1024f53e11; +}
\ No newline at end of file diff --git a/Test/floats/float7.bpl.expect b/Test/floats/float7.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/floats/float7.bpl.expect @@ -0,0 +1,2 @@ +
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/floats/float8.bpl b/Test/floats/float8.bpl new file mode 100644 index 00000000..bfb3b9e9 --- /dev/null +++ b/Test/floats/float8.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() returns () { + var x : float24e8; + var y : float24e8; + var z : float24e8; + var r : float24e8; + x := 0e167f24e8; + y := x + 0e127f24e8; + z := x - 0e127f24e8; + r := y - z; + assert r == 0e128f24e8; +}
\ No newline at end of file diff --git a/Test/floats/float8.bpl.expect b/Test/floats/float8.bpl.expect new file mode 100644 index 00000000..426c21e0 --- /dev/null +++ b/Test/floats/float8.bpl.expect @@ -0,0 +1,5 @@ +float8.bpl(12,2): Error BP5001: This assertion might not hold.
+Execution trace:
+ float8.bpl(8,4): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/floats/float9.bpl b/Test/floats/float9.bpl new file mode 100644 index 00000000..b1e46ae4 --- /dev/null +++ b/Test/floats/float9.bpl @@ -0,0 +1,17 @@ +// 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); + +procedure main() returns () { + var x : float24e8; + var y : float24e8; + var z : float24e8; + var r : float24e8; + 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/float9.bpl.expect b/Test/floats/float9.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/floats/float9.bpl.expect @@ -0,0 +1,2 @@ +
+Boogie program verifier finished with 1 verified, 0 errors
|