summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2016-10-29 17:35:13 -0400
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2016-10-29 17:35:13 -0400
commit1f2d6c15cc587e9e1b91be70186ee9a26d5e1928 (patch)
tree1b6cd99944efbba2c993327bb49f2d544d50b1eb /Test
parent41082463d783d6f8d8a5aaf69bf459b57bca6000 (diff)
parentba4f9fa1fbd923bfce1363566af08624c5c6fe38 (diff)
Merge branch 'upstream' into dfsg_freedfsg_free
Diffstat (limited to 'Test')
-rw-r--r--Test/civl/ticket.bpl25
-rw-r--r--Test/civl/ticket.bpl.expect2
-rw-r--r--Test/floats/float0.bpl14
-rw-r--r--Test/floats/float0.bpl.expect8
-rw-r--r--Test/floats/float1.bpl13
-rw-r--r--Test/floats/float1.bpl.expect2
-rw-r--r--Test/floats/float10.bpl18
-rw-r--r--Test/floats/float10.bpl.expect5
-rw-r--r--Test/floats/float11.bpl22
-rw-r--r--Test/floats/float11.bpl.expect7
-rw-r--r--Test/floats/float12.bpl16
-rw-r--r--Test/floats/float12.bpl.expect2
-rw-r--r--Test/floats/float13.bpl34
-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/float2.bpl15
-rw-r--r--Test/floats/float2.bpl.expect7
-rw-r--r--Test/floats/float3.bpl27
-rw-r--r--Test/floats/float3.bpl.expect2
-rw-r--r--Test/floats/float4.bpl19
-rw-r--r--Test/floats/float4.bpl.expect2
-rw-r--r--Test/floats/float5.bpl23
-rw-r--r--Test/floats/float5.bpl.expect6
-rw-r--r--Test/floats/float6.bpl30
-rw-r--r--Test/floats/float6.bpl.expect2
-rw-r--r--Test/floats/float7.bpl13
-rw-r--r--Test/floats/float7.bpl.expect2
-rw-r--r--Test/floats/float8.bpl13
-rw-r--r--Test/floats/float8.bpl.expect5
-rw-r--r--Test/floats/float9.bpl17
-rw-r--r--Test/floats/float9.bpl.expect2
32 files changed, 378 insertions, 8 deletions
diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl
index df19aae4..2e0c6cd1 100644
--- a/Test/civl/ticket.bpl
+++ b/Test/civl/ticket.bpl
@@ -7,7 +7,7 @@ axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
type X;
const nil: X;
-var {:layer 0,2} t: int;
+var {:layer 0,1} t: int;
var {:layer 0,2} s: int;
var {:layer 0,2} cs: X;
var {:layer 0,2} T: [int]bool;
@@ -41,14 +41,15 @@ ensures {:layer 1} {:layer 2} xl != nil;
}
procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)
-requires {:layer 2} xls' == MapConstBool(true);
+requires {:layer 1} Inv1(T, t);
+requires {:layer 2} xls' == MapConstBool(true) && Inv2(T, s, cs);
{
var {:linear "tid"} tid: X;
var {:linear "tid"} xls: [X]bool;
- yield;
+ par Yield1() | Yield2();
- call Init(xls');
+ call InitAbstract(xls');
xls := xls';
par Yield1() | Yield2();
@@ -96,10 +97,20 @@ ensures {:layer 2} Inv2(T, s, cs) && cs == tid;
par Yield1() | Yield2() | YieldSpec(tid);
}
+procedure {:yields} {:layer 1,2} InitAbstract({:linear "tid"} xls:[X]bool)
+requires {:layer 1} Inv1(T, t);
+ensures {:layer 1} Inv1(T, t);
+ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; s := 0; T := RightOpen(0); return true; }|;
+{
+ par Yield1();
+ call Init(xls);
+ par Yield1();
+}
+
procedure {:yields} {:layer 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int)
requires {:layer 1} Inv1(T, t);
ensures {:layer 1} Inv1(T, t);
-ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|;
+ensures {:right} |{ A: havoc m; assume !T[m]; T[m] := true; return true; }|;
{
par Yield1();
call m := GetTicket(tid);
@@ -130,7 +141,7 @@ ensures {:layer 1} Inv1(T,t);
assert {:layer 1} Inv1(T,t);
}
-procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool);
+procedure {:yields} {:layer 0,1} Init({:linear "tid"} xls:[X]bool);
ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);
@@ -140,7 +151,7 @@ procedure {:yields} {:layer 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int);
ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|;
procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X);
-ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|;
+ensures {:atomic} |{ A: assert cs == tid; s := s + 1; cs := nil; return true; }|;
procedure {:yields} {:layer 0,2} AllocateLow({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);
ensures {:atomic} |{ A: assume xl != nil; return true; }|;
diff --git a/Test/civl/ticket.bpl.expect b/Test/civl/ticket.bpl.expect
index dc45a0ee..6696bdbd 100644
--- a/Test/civl/ticket.bpl.expect
+++ b/Test/civl/ticket.bpl.expect
@@ -1,2 +1,2 @@
-Boogie program verifier finished with 24 verified, 0 errors
+Boogie program verifier finished with 26 verified, 0 errors
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..b60994d4
--- /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..213345cb
--- /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..37fad75c
--- /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..37fad75c
--- /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..c55c4619
--- /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..37fad75c
--- /dev/null
+++ b/Test/floats/float9.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors