summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Checkmate50 <dgeisler50@gmail.com>2016-06-06 21:09:06 -0600
committerGravatar Checkmate50 <dgeisler50@gmail.com>2016-06-06 21:09:06 -0600
commit5cff8cd77c629ec8e48a2498b1e704173306586a (patch)
tree8ab0b6fbda08b12e9b2635efdb5806371197c58c
parentc19c2495497d0dfa7aaf871cf833cd5e5f986d33 (diff)
finished testing, fixed several minor compiler bugs
-rw-r--r--Source/Basetypes/BigFloat.cs2
-rw-r--r--Source/Core/Parser.cs82
-rw-r--r--Source/Provers/SMTLib/SMTLibProcess.cs2
-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.bpl23
-rw-r--r--Test/floats/float14.bpl17
-rw-r--r--Test/floats/float15.bpl (renamed from Test/floats/test5.bpl)0
-rw-r--r--Test/floats/float16.bpl (renamed from Test/floats/test6.bpl)0
-rw-r--r--Test/floats/float17.bpl (renamed from Test/floats/test7.bpl)0
-rw-r--r--Test/floats/float18.bpl (renamed from Test/floats/test8.bpl)0
-rw-r--r--Test/floats/float19.bpl (renamed from Test/floats/test9.bpl)0
-rw-r--r--Test/floats/float2.bpl15
-rw-r--r--Test/floats/float2.bpl.expect7
-rw-r--r--Test/floats/float20.bpl (renamed from Test/floats/test20.bpl)0
-rw-r--r--Test/floats/float21.bpl35
-rw-r--r--Test/floats/float22.bpl (renamed from Test/floats/test14.bpl)0
-rw-r--r--Test/floats/float23.bpl (renamed from Test/floats/test16.bpl)0
-rw-r--r--Test/floats/float3.bpl27
-rw-r--r--Test/floats/float3.bpl.expect2
-rw-r--r--Test/floats/float4.bpl11
-rw-r--r--Test/floats/float4.bpl.expect2
-rw-r--r--Test/floats/float5.bpl24
-rw-r--r--Test/floats/float5.bpl.expect9
-rw-r--r--Test/floats/float6.bpl50
-rw-r--r--Test/floats/float6.bpl.expect2
-rw-r--r--Test/floats/float7.bpl (renamed from Test/floats/test1.bpl)24
-rw-r--r--Test/floats/float7.bpl.expect2
-rw-r--r--Test/floats/float8.bpl (renamed from Test/floats/test3.bpl)24
-rw-r--r--Test/floats/float8.bpl.expect5
-rw-r--r--Test/floats/float9.bpl (renamed from Test/floats/test2.bpl)32
-rw-r--r--Test/floats/float9.bpl.expect2
-rw-r--r--Test/floats/modpath.py13
-rw-r--r--Test/floats/test10.bpl20
-rw-r--r--Test/floats/test11.bpl55
-rw-r--r--Test/floats/test12.bpl43
-rw-r--r--Test/floats/test13.bpl19
-rw-r--r--Test/floats/test15.bpl24
-rw-r--r--Test/floats/test17.bpl11
-rw-r--r--Test/floats/test18.bpl36
-rw-r--r--Test/floats/test19.bpl36
-rw-r--r--Test/floats/test4.bpl32
50 files changed, 444 insertions, 351 deletions
diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index a0ce03a5..3c4cc40a 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -313,7 +313,7 @@ namespace Microsoft.Basetypes
return "_ " + this.value + " " + this.exponentSize + " " + this.significandSize;
}
else if (this.Value == "") {
- return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + this.significandSize + ")";
+ return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + (this.significandSize-1) + ")";
}
else {
return "(_ to_fp " + this.exponentSize + " " + this.significandSize + ") (_ bv" + this.value + " " + (this.exponentSize + this.significandSize).ToString() + ")";
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 8161544f..7982f594 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -668,35 +668,7 @@ private class BvBounds : Expr {
ty = new BasicType(t, SimpleType.Real);
} else if (la.kind == 98) {
Get();
- if (t.val.Length > 5) {
- switch (Int32.Parse(t.val.Substring(5))) {
- case 16:
- ty = new FloatType(t, 5, 11);
- break;
- case 32:
- ty = new FloatType(t, 8, 24);
- break;
- case 64:
- ty = new FloatType(t, 11, 53);
- break;
- case 128:
- ty = new FloatType(t, 15, 113);
- break;
- default:
- SynErr(3);
- break;
- }
- }
- else {
- Expect(19); //<
- Expect(3); //int
- int exp = Int32.Parse(t.val);
- Expect(12); //,
- Expect(3); //int
- int man = Int32.Parse(t.val);
- ty = new FloatType(t, exp, man);
- Expect(20); //>
- }
+ ty = FType();
} else if (la.kind == 16) {
Get();
ty = new BasicType(t, SimpleType.Bool);
@@ -707,6 +679,39 @@ private class BvBounds : Expr {
} else SynErr(101);
}
+ FloatType FType() {
+ if (t.val.Length > 5) {
+ switch (Int32.Parse(t.val.Substring(5))) {
+ case 16:
+ return new FloatType(t, 5, 11);
+ case 32:
+ return new FloatType(t, 8, 24);
+ case 64:
+ return new FloatType(t, 11, 53);
+ case 128:
+ return new FloatType(t, 15, 113);
+ default:
+ SynErr(3);
+ return new FloatType(t, 0, 0);
+ }
+ }
+ else {
+ try {
+ Expect(19); //<
+ Expect(3); //int
+ int exp = Int32.Parse(t.val);
+ Expect(12); //,
+ Expect(3); //int
+ int man = Int32.Parse(t.val);
+ Expect(20); //>
+ return new FloatType(t, exp, man);
+ }
+ catch (Exception) {
+ return new FloatType(t, 0, 0);
+ }
+ }
+ }
+
void Ident(out IToken/*!*/ x) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null);
Expect(1);
@@ -1915,8 +1920,13 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Get(); //Skip the float token
if (la.val == "(") {
Get();
- Expect(16); //bool
- negative = Boolean.Parse(t.val);
+ if (la.val == "false")
+ negative = false;
+ else if (la.val == "true")
+ negative = true;
+ else
+ throw new FormatException();
+ Get();
Expect(12); //,
BvLit(out exp_val, out exp);
Expect(12);
@@ -1933,10 +1943,16 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
sig = Int32.Parse(t.val);
Expect(20); //>
Expect(9); //(
- if (la.kind == 4) {
+ if (la.kind == 1) { //NaN
Get();
n = new BigFloat(t.val, exp, sig);
}
+ else if (la.kind == 74 || la.kind == 75) { //+ or -
+ Get();
+ String s = t.val;
+ Get();
+ n = new BigFloat(s + t.val, exp, sig);
+ }
else {
BvLit(out value, out size);
n = new BigFloat(value.ToString(), exp, sig);
@@ -2194,7 +2210,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
{x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x},
{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 4982d81e..bc94e253 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -93,7 +93,7 @@ namespace Microsoft.Boogie.SMTLib
log = log.Replace("\r", "").Replace("\n", " ");
Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log);
}
- Console.WriteLine(cmd);
+ //Console.WriteLine(cmd);
toProver.WriteLine(cmd);
}
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..6abb715b
--- /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..19e55fef
--- /dev/null
+++ b/Test/floats/float11.bpl.expect
@@ -0,0 +1,7 @@
+..\Test\floats\float11.bpl(21,2): Error BP5001: This assertion might not hold.
+Execution trace:
+ ..\Test\floats\float11.bpl(12,7): anon0
+ ..\Test\floats\float11.bpl(16,2): anon3_LoopHead
+ ..\Test\floats\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..6abb715b
--- /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..4fe25140
--- /dev/null
+++ b/Test/floats/float13.bpl
@@ -0,0 +1,23 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+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 : float64;
+
+ havoc x;
+ assume(x >= TO_FLOAT64_INT(0) && x <= TO_FLOAT64_INT(10));
+
+ y := x*x - x;
+ if (y >= TO_FLOAT64_INT(0)) {
+ y := x / TO_FLOAT64_INT(10);
+ }
+ else {
+ y := x*x + TO_FLOAT64_INT(2);
+ }
+
+ assert(y >= TO_FLOAT64_INT(0) && y <= TO_FLOAT64_INT(105));
+} \ No newline at end of file
diff --git a/Test/floats/float14.bpl b/Test/floats/float14.bpl
new file mode 100644
index 00000000..46c1b07d
--- /dev/null
+++ b/Test/floats/float14.bpl
@@ -0,0 +1,17 @@
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+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 : float64;
+ var r : float64;
+
+ x := TO_FLOAT64_INT(77617);
+ y := TO_FLOAT64_INT(33096);
+ r := y*y*y*y*y*y * TO_FLOAT64_REAL(333.75) + x*x * (x*x*y*y*TO_FLOAT64_INT(11) - y*y*y*y*y*y - y*y*y*y * TO_FLOAT64_INT(121) - TO_FLOAT64_INT(2)) + y*y*y*y*y*y*y*y * TO_FLOAT64_REAL(5.5) + x / (y*TO_FLOAT64_INT(2));
+
+ assert(r >= TO_FLOAT64_INT(0));
+} \ No newline at end of file
diff --git a/Test/floats/test5.bpl b/Test/floats/float15.bpl
index 7536f8fd..7536f8fd 100644
--- a/Test/floats/test5.bpl
+++ b/Test/floats/float15.bpl
diff --git a/Test/floats/test6.bpl b/Test/floats/float16.bpl
index 6bef1137..6bef1137 100644
--- a/Test/floats/test6.bpl
+++ b/Test/floats/float16.bpl
diff --git a/Test/floats/test7.bpl b/Test/floats/float17.bpl
index 8e07878d..8e07878d 100644
--- a/Test/floats/test7.bpl
+++ b/Test/floats/float17.bpl
diff --git a/Test/floats/test8.bpl b/Test/floats/float18.bpl
index 7e78e206..7e78e206 100644
--- a/Test/floats/test8.bpl
+++ b/Test/floats/float18.bpl
diff --git a/Test/floats/test9.bpl b/Test/floats/float19.bpl
index c3a42e6b..c3a42e6b 100644
--- a/Test/floats/test9.bpl
+++ b/Test/floats/float19.bpl
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/test20.bpl b/Test/floats/float20.bpl
index 57c605fd..57c605fd 100644
--- a/Test/floats/test20.bpl
+++ b/Test/floats/float20.bpl
diff --git a/Test/floats/float21.bpl b/Test/floats/float21.bpl
new file mode 100644
index 00000000..5fad5859
--- /dev/null
+++ b/Test/floats/float21.bpl
@@ -0,0 +1,35 @@
+// 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;
+
+ havoc x;
+ assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1));
+
+ if (x != TO_FLOAT32_INT(0)) {
+ y := x * x;
+ assert(y != TO_FLOAT32_INT(0));
+ z := TO_FLOAT32_INT(1) / y;
+ }
+}
+
+procedure main() returns () {
+ var x : float32;
+ var y : float32;
+ var z : float32;
+
+ havoc x;
+ assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1));
+
+ if (x <= TO_FLOAT32_REAL(-1e-20) || x >= TO_FLOAT32_REAL(1e-20)) {
+ y := x * x;
+ assert(y != TO_FLOAT32_INT(0));
+ z := TO_FLOAT32_INT(1) / y;
+ }
+} \ No newline at end of file
diff --git a/Test/floats/test14.bpl b/Test/floats/float22.bpl
index 1505c361..1505c361 100644
--- a/Test/floats/test14.bpl
+++ b/Test/floats/float22.bpl
diff --git a/Test/floats/test16.bpl b/Test/floats/float23.bpl
index 69ae243d..69ae243d 100644
--- a/Test/floats/test16.bpl
+++ b/Test/floats/float23.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..6abb715b
--- /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..6abb715b
--- /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/test1.bpl b/Test/floats/float7.bpl
index e893e098..f330b2ea 100644
--- a/Test/floats/test1.bpl
+++ b/Test/floats/float7.bpl
@@ -1,13 +1,13 @@
-//Translation from addsub_double_exact.c
-//Should Verify
-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);
+// 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/test3.bpl b/Test/floats/float8.bpl
index 67c6ba48..78c11a2b 100644
--- a/Test/floats/test3.bpl
+++ b/Test/floats/float8.bpl
@@ -1,13 +1,13 @@
-//Translation from addsub_float_inexact.c
-//Should give an error
-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);
+// 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/test2.bpl b/Test/floats/float9.bpl
index d78c339d..cb4f3afd 100644
--- a/Test/floats/test2.bpl
+++ b/Test/floats/float9.bpl
@@ -1,17 +1,17 @@
-//Translation from addsub_float_exact.c
-//Should Verify
-
-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);
+// 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/floats/modpath.py b/Test/floats/modpath.py
new file mode 100644
index 00000000..90707701
--- /dev/null
+++ b/Test/floats/modpath.py
@@ -0,0 +1,13 @@
+import sys
+
+f = open(sys.argv[1], 'r')
+to_write = ""
+
+for i in f:
+ to_write += i.replace("..\\Test\\floats\\", "")
+
+f.close()
+
+f = open(sys.argv[1], 'w')
+
+f.write(to_write) \ No newline at end of file
diff --git a/Test/floats/test10.bpl b/Test/floats/test10.bpl
deleted file mode 100644
index 566f7a56..00000000
--- a/Test/floats/test10.bpl
+++ /dev/null
@@ -1,20 +0,0 @@
-//Translation from loop.c
-//Should return an error? (The real case does as well...)
-
-procedure main() returns () {
- var x : float;
- var y : float;
- var z : float;
-
- x := fp(1);
- y := fp(10000000);
- z := fp(42);
-
- while (x < y) {
- x := x + fp(1);
- y := y - fp(1);
- z := z + fp(1);
- }
-
- assert(z >= fp(0) && z <= fp(10000000));
-} \ No newline at end of file
diff --git a/Test/floats/test11.bpl b/Test/floats/test11.bpl
deleted file mode 100644
index cee3e36e..00000000
--- a/Test/floats/test11.bpl
+++ /dev/null
@@ -1,55 +0,0 @@
-//Translation from interpolation.c
-//Should Verify
-//Returns inconclusive? What does that mean?
-
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);
-procedure main() returns () {
- var i : int;
- var z : float32;
- var t : float32;
- var min : [int] float32;
- var max : [int] float32;
-
- min[0] := TO_FLOAT32_INT(5);
- min[1] := TO_FLOAT32_INT(10);
- min[2] := TO_FLOAT32_INT(12);
- min[3] := TO_FLOAT32_INT(30);
- min[4] := TO_FLOAT32_INT(150);
-
- max[0] := TO_FLOAT32_INT(10);
- max[1] := TO_FLOAT32_INT(12);
- max[2] := TO_FLOAT32_INT(30);
- max[3] := TO_FLOAT32_INT(150);
- max[4] := TO_FLOAT32_INT(300);
-
- havoc t;
- assume(t >= min[0] && t <= max[4]);
-
- i := 0;
- //while (i < 5) {
- //if (t <= max[i]) {
- //break;
- //}
- //i := i + 1;
- //}
-
- if (t > max[0]) { //1
- i := i + 1;
- }
- if (t > max[1]) { //2
- i := i + 1;
- }
- if (t > max[2]) { //3
- i := i + 1;
- }
- if (t > max[3]) { //4
- i := i + 1;
- }
- if (t > max[4]) { //5
- i := i + 1;
- }
-
- z := (t - min[i]) / (max[i] - min[i]);
-
- assert(z >= TO_FLOAT32_INT(0) && z <= TO_FLOAT32_INT(1));
-} \ No newline at end of file
diff --git a/Test/floats/test12.bpl b/Test/floats/test12.bpl
deleted file mode 100644
index c733b9f4..00000000
--- a/Test/floats/test12.bpl
+++ /dev/null
@@ -1,43 +0,0 @@
-//Translation from inv_Newton.c
-//Should Verify
-//Unfinished code!
-
-procedure inv(float(11 53)) returns(float(11 53)) {
- var z : float(11 53);
- var t : float(11 53);
- var t : float(11 53);
-
-
-}
-
-procedure main() returns () {
- var t : float(11 53);
- var t : float(11 53);
-
- min[0] := fp(5);
- min[1] := fp(10);
- min[2] := fp(12);
- min[3] := fp(30);
- min[4] := fp(150);
-
- max[0] := fp(10);
- max[1] := fp(12);
- max[2] := fp(30);
- max[3] := fp(150);
- max[4] := fp(300);
-
- havoc t;
- assume(t >= min[0] && t <= max[4]);
-
- i := 0;
- while (i < 5) {
- if (t <= max[i]) {
- break;
- }
- i := i + 1;
- }
-
- z := (t - min[i]) / (max[i] - min[i]);
-
- assert(z >= fp(0) && z <= fp(1));
-} \ No newline at end of file
diff --git a/Test/floats/test13.bpl b/Test/floats/test13.bpl
deleted file mode 100644
index e5402539..00000000
--- a/Test/floats/test13.bpl
+++ /dev/null
@@ -1,19 +0,0 @@
-//Translation from inv_square_false-unreach-call.c
-//Should return an error (without crashing)
-
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);
-
-procedure main() returns () {
- var x : float32;
- var y : float32;
- var z : float32;
-
- havoc x;
- assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1));
-
- if (x != TO_FLOAT32_INT(0)) {
- y := x * x;
- assert(y != TO_FLOAT32_INT(0));
- z := TO_FLOAT32_INT(1) / y;
- }
-} \ No newline at end of file
diff --git a/Test/floats/test15.bpl b/Test/floats/test15.bpl
deleted file mode 100644
index 1dc549ac..00000000
--- a/Test/floats/test15.bpl
+++ /dev/null
@@ -1,24 +0,0 @@
-//Translation from Muller_Kahan.c
-//Should Verify
-//NOTE: (fp(....)) causes a compiler error!
-//FAILS! Heavily...
-
-procedure main() returns () {
- var x0 : float(11 53);
- var x1 : float(11 53);
- var x2 : float(11 53);
- var i : int;
-
- x0 := fp(11 11 53) / fp(2 11 53);
- x1 := fp(61 11 53) / fp(11 11 53);
- i := 0;
- while (i < 100) {
- x2 := fp(1130 11 53) - fp(3000 11 53) / x0;
- x2 := fp(111 11 53) - x2 / x1;
- x0 := x1;
- x1 := x2;
- i := i + 1;
- }
-
- assert(x0 >= fp(99 11 53) && x0 <= fp(101 11 53));
-} \ No newline at end of file
diff --git a/Test/floats/test17.bpl b/Test/floats/test17.bpl
deleted file mode 100644
index caa1fa74..00000000
--- a/Test/floats/test17.bpl
+++ /dev/null
@@ -1,11 +0,0 @@
-//Translation from nan_double_range_true-unreach-call.c
-//Should verify
-//Uggghhhh, should I add support for e?
-
-procedure main() returns () {
- var x : float(11 53);
- havoc x;
- if (x >= fp(-100000000000000000000000000 11 53) && x <= fp(100000000000000000000000000 11 53)) {
- assert(x==x);
- }
-} \ No newline at end of file
diff --git a/Test/floats/test18.bpl b/Test/floats/test18.bpl
deleted file mode 100644
index 71eb5286..00000000
--- a/Test/floats/test18.bpl
+++ /dev/null
@@ -1,36 +0,0 @@
-//Translation from rlim_exit.c
-//Should verify
-//Unary - unsupported float operations (on my end)...
-
-procedure main() returns () {
- var X : float;
- var Y : float;
- var S : float;
- var R : float;
- var D : float;
- var i : int;
-
- Y := fp(0);
-
- i := 0;
- while (i < 100000) {
- havoc X;
- havoc D;
- assume(X >= fp(-128) && X <= fp(128));
- assume(D >= fp(0) && D <= fp(16));
-
- S := Y;
- Y := X;
- R := X - S;
- if (R <= fp(0)-D) {
- Y := S - D;
- }
- else if(R >= D) {
- Y := S + D;
- }
-
- i := i + 1;
- }
-
- assert(Y >= fp(-129) && Y <= fp(129));
-} \ No newline at end of file
diff --git a/Test/floats/test19.bpl b/Test/floats/test19.bpl
deleted file mode 100644
index f00d8a2b..00000000
--- a/Test/floats/test19.bpl
+++ /dev/null
@@ -1,36 +0,0 @@
-//Translation from flim_invariant.c
-//Should verify
-//Unary - unsupported float operations (on my end)...
-
-procedure main() returns () {
- var X : float;
- var Y : float;
- var S : float;
- var R : float;
- var D : float;
- var i : int;
-
- Y := fp(0);
-
- i := 0;
- while (i < 100000) {
- havoc X;
- havoc D;
- assume(X >= fp(-128) && X <= fp(128));
- assume(D >= fp(0) && D <= fp(16));
-
- S := Y;
- Y := X;
- R := X - S;
- if (R <= fp(0)-D) {
- Y := S - D;
- }
- else if(R >= D) {
- Y := S + D;
- }
-
- assert(Y >= fp(-129) && Y <= fp(129));
-
- i := i + 1;
- }
-} \ No newline at end of file
diff --git a/Test/floats/test4.bpl b/Test/floats/test4.bpl
deleted file mode 100644
index a31aa215..00000000
--- a/Test/floats/test4.bpl
+++ /dev/null
@@ -1,32 +0,0 @@
-//Translation from drift_tenth.c
-//Should Fail
-
-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;
- //}
- time := time + tick;//1
- time := time + tick;//2
- time := time + tick;//3
- time := time + tick;//4
- time := time + tick;//5
- time := time + tick;//6
- time := time + tick;//7
- time := time + tick;//8
- time := time + tick;//9
- time := time + tick;//10
- assert time == TO_FLOAT32_INT(1);
-} \ No newline at end of file