summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Test/floats/float1.bpl10
-rw-r--r--Test/floats/float13.bpl30
-rw-r--r--Test/floats/float13.bpl.expect2
-rw-r--r--Test/floats/float14.bpl22
-rw-r--r--Test/floats/float14.bpl.expect9
-rw-r--r--Test/floats/float3.bpl18
-rw-r--r--Test/floats/float4.bpl10
-rw-r--r--Test/floats/float7.bpl8
-rw-r--r--Test/floats/float8.bpl8
9 files changed, 94 insertions, 23 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 18:55:11 +0000