diff options
Diffstat (limited to 'Test')
27 files changed, 310 insertions, 2 deletions
diff --git a/Test/floats/float0.bpl b/Test/floats/float0.bpl new file mode 100644 index 00000000..b1a240be --- /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 : float<8, 24>) +{ + r := 15; // Error + r := 15.0; // Error + r := fp(false, 1bv8, 0bv22); // Error + r := fp<8, 23>(1bv31); // Error + r := x; // Error + r := fp<8, 23>(1bv31) + fp<8, 23>(1bv31); // Error + r := fp<8, 24>(1bv32) + fp<8, 23>(1bv31); // 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..4c934700 --- /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 float (8 24))
+float0.bpl(6,1): Error: mismatched types in assignment command (cannot assign real to float (8 24))
+float0.bpl(7,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float0.bpl(8,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float0.bpl(9,1): Error: mismatched types in assignment command (cannot assign real to float (8 24))
+float0.bpl(10,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float0.bpl(11,23): Error: invalid argument types (float (8 24) and float (8 23)) 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..9ed62579 --- /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 : float<8, 24>) returns (r : float<8, 24>)
+{
+ r := fp(false, 1bv8, 0bv23);
+ r := fp<8, 24>(1bv32);
+ r := x;
+ r := x + fp<8, 24>(1bv32);
+ r := fp<8, 24>(1bv32) + fp<8, 24>(1bv32);
+ assert(r == fp<8, 24>(2bv32));
+
+ 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..bf07aec6 --- /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 (float64); + +procedure double_range_true() returns () { + var x : float64; + havoc x; + if (x >= TO_FLOAT64_REAL(-1e307) && x <= TO_FLOAT64_REAL(1e307)) { + assert(x==x); + } +} + +procedure double_range_false() returns () { + var x : float64; + 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..424c5a2d --- /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 (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;
+ }
+ 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..349abb41 --- /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(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/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/float2.bpl b/Test/floats/float2.bpl new file mode 100644 index 00000000..1a4d02cd --- /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 : float16) returns(r : float32) {
+ var y : float64;
+ var z : float128;
+
+ 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..62348741 --- /dev/null +++ b/Test/floats/float2.bpl.expect @@ -0,0 +1,7 @@ +float2.bpl(7,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (8 24))
+float2.bpl(8,1): Error: mismatched types in assignment command (cannot assign float (11 53) to float (8 24))
+float2.bpl(9,1): Error: mismatched types in assignment command (cannot assign float (15 113) to float (8 24))
+float2.bpl(10,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (11 53))
+float2.bpl(11,1): Error: mismatched types in assignment command (cannot assign float (15 113) to float (11 53))
+float2.bpl(12,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (15 113))
+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..34059f80 --- /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 : float32;
+ var y : float32;
+ var z : float32;
+
+ z := x + y;
+ z := x - y;
+ z := x * y;
+ assume(y != fp<8, 24>(0bv32));
+ z := x / y;
+
+ z := (fp<8, 24>(1bv32) + fp<8, 24>(1bv32)) + fp<8, 24>(0bv32);
+ assert(z == fp<8, 24>(2bv32));
+
+ z := fp<8, 24>(2bv32) - fp<8, 24>(1bv32);
+ assert(z == fp<8, 24>(1bv32));
+
+ z := fp(false, 127bv8, 0bv23) * fp(false, 127bv8, 0bv23);
+ assert(z == fp(false, 127bv8, 0bv23));
+
+ z := fp<8, 24>(1bv32) / fp<8, 24>(1bv32);
+ assert(z == fp(false, 127bv8, 0bv23));
+
+ 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..7bb24250 --- /dev/null +++ b/Test/floats/float4.bpl @@ -0,0 +1,11 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo() returns (r : float32) {
+ r := fp<8, 24>(NaN);
+ r := fp<8, 24>(+oo);
+ r := fp<8, 24>(-oo);
+ r := fp<8, 24>(+zero);
+ r := fp<8, 24>(-zero);
+
+ 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..fd630394 --- /dev/null +++ b/Test/floats/float5.bpl @@ -0,0 +1,24 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_INT(int) returns (float<8, 23>);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_REAL(real) returns (float<8, 23>);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV31(bv31) returns (float<8, 23>);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV32(bv32) returns (float<8, 23>);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_FLOAT824(float<8, 24>) returns (float<8, 23>);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_FLOAT823(float<8, 23>) returns (float<8, 24>);
+
+procedure foo(x : float<8, 24>) returns (r : float<8, 24>) {
+ 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(fp<8, 24>(1bv32)); // Error
+ r := TO_FLOAT824_FLOAT823(fp<8, 24>(1bv32)); // Error
+ r := TO_FLOAT824_FLOAT823(fp<8, 23>(1bv31));
+
+ 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..6c0b86af --- /dev/null +++ b/Test/floats/float5.bpl.expect @@ -0,0 +1,9 @@ +float5.bpl(12,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float5.bpl(13,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float5.bpl(14,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float5.bpl(15,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float5.bpl(16,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float5.bpl(17,42): Error: invalid type for argument 0 in application of TO_FLOAT824_FLOAT823: float (8 24) (expected: float (8 23))
+float5.bpl(20,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float5.bpl(21,27): Error: invalid type for argument 0 in application of TO_FLOAT824_FLOAT823: float (8 24) (expected: float (8 23))
+8 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..fe0eab0e --- /dev/null +++ b/Test/floats/float6.bpl @@ -0,0 +1,50 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_INT(int) returns (float<8, 24>);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_REAL(real) returns (float<8, 24>);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_BV32(bv32) returns (float<8, 24>);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT1153_BV64(bv64) returns (float<11, 53>);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_FLOAT32(float32) returns (float<8, 24>); //Should just be an identity function
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT824(float<8, 24>) returns (float32); //Should just be an identity function
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float64) returns (float32);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float32) returns (float64);
+
+procedure main() returns () {
+ var i : int;
+ var r : real;
+ var f824 : float<8, 24>;
+ var f32 : float32;
+ var f1153 : float<11, 53>;
+ var f64 : float64;
+
+ f824 := TO_FLOAT824_INT(5);
+ f32 := TO_FLOAT824_INT(5);
+ f824 := TO_FLOAT824_REAL(5.0);
+ f32 := TO_FLOAT824_REAL(5.0);
+
+ f824 := TO_FLOAT824_BV32(0bv32);
+ f32 := TO_FLOAT824_BV32(0bv32);
+ f1153 := TO_FLOAT1153_BV64(0bv64);
+ f64 := TO_FLOAT1153_BV64(0bv64);
+
+ f824 := TO_FLOAT824_FLOAT32(fp<8, 24>(0bv32));
+ f32 := TO_FLOAT32_FLOAT824(fp<8, 24>(0bv32));
+ f824 := TO_FLOAT32_FLOAT64(fp<11, 53>(0bv32));
+ f32 := TO_FLOAT32_FLOAT64(fp<11, 53>(0bv32));
+ f1153 := TO_FLOAT64_FLOAT32(fp<8, 24>(0bv32));
+ f64 := TO_FLOAT64_FLOAT32(fp<8, 24>(0bv32));
+
+ f824 := TO_FLOAT824_INT(5);
+ f32 := TO_FLOAT32_FLOAT824(f824);
+ assert(f32 == f824);
+
+ f32 := TO_FLOAT824_INT(5);
+ f824 := TO_FLOAT824_FLOAT32(f32);
+ assert(f32 == f824);
+
+ 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..f330b2ea --- /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 : 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/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..78c11a2b --- /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 : 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/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..cb4f3afd --- /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 (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/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
diff --git a/Test/test1/IntReal.bpl.expect b/Test/test1/IntReal.bpl.expect index 021a8389..b532d22a 100644 --- a/Test/test1/IntReal.bpl.expect +++ b/Test/test1/IntReal.bpl.expect @@ -12,8 +12,8 @@ IntReal.bpl(19,12): Error: invalid argument types (real and int) to binary opera IntReal.bpl(25,8): Error: invalid argument types (int and real) to binary operator ** IntReal.bpl(29,14): Error: invalid argument types (real and int) to binary operator == IntReal.bpl(31,13): Error: invalid argument types (int and real) to binary operator == -IntReal.bpl(34,6): Error: argument type int does not match expected type real -IntReal.bpl(35,6): Error: argument type real does not match expected type int +IntReal.bpl(34,6): Error: argument type int does not match expected type real or type float +IntReal.bpl(35,6): Error: argument type real does not match expected type int or type float IntReal.bpl(47,8): Error: invalid argument types (real and int) to binary operator div IntReal.bpl(48,8): Error: invalid argument types (real and int) to binary operator mod 18 type checking errors detected in IntReal.bpl |