summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/Parser.cs27
-rw-r--r--Source/Core/Scanner.cs2
-rw-r--r--float_test11.bpl57
-rw-r--r--float_test13.bpl16
-rw-r--r--float_test14.bpl19
-rw-r--r--float_test2.bpl20
-rw-r--r--float_test3.bpl16
-rw-r--r--float_test4.bpl38
-rw-r--r--float_test5.bpl13
-rw-r--r--float_test8.bpl16
10 files changed, 134 insertions, 90 deletions
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 77100d1c..8161544f 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -668,9 +668,8 @@ private class BvBounds : Expr {
ty = new BasicType(t, SimpleType.Real);
} else if (la.kind == 98) {
Get();
- if (la.kind == 3) {
- Get();
- switch (Int32.Parse(t.val)) {
+ if (t.val.Length > 5) {
+ switch (Int32.Parse(t.val.Substring(5))) {
case 16:
ty = new FloatType(t, 5, 11);
break;
@@ -690,10 +689,10 @@ private class BvBounds : Expr {
}
else {
Expect(19); //<
- Expect(3);
+ Expect(3); //int
int exp = Int32.Parse(t.val);
Expect(12); //,
- Expect(3);
+ Expect(3); //int
int man = Int32.Parse(t.val);
ty = new FloatType(t, exp, man);
Expect(20); //>
@@ -1830,14 +1829,14 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
break;
}
case 98: {
- Get();
- x = t;
- Expect(19);
- Expression(out e);
- Expect(20);
- e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToFloat), new List<Expr> { e });
- break;
- }
+ Get();
+ x = t;
+ Expect(19);
+ Expression(out e);
+ Expect(20);
+ e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToFloat), new List<Expr> { e });
+ break;
+ }
case 9: {
Get();
if (StartOf(9)) {
@@ -2188,7 +2187,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
static readonly bool[,]/*!*/ set = { //grid is 17 x 100
{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,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,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,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,T,x,x, x,x,T,T, T,T,x,T, 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,x, x,x,x,x, x,x,x,x, x,x,x,x},
+ {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,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,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,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,T, 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,T,x,x, x,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, x,x,x,x, x,x,x,x, x,x,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},
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index bc294aba..ca7db1e1 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -509,7 +509,7 @@ public class Scanner {
case "real": t.kind = 15; break;
case "bool": t.kind = 16; break;
case "fp": t.kind = 97; break;
- case "float": t.kind = 98; break;
+ case "float": case "float16": case "float32": case "float64": case "float128": t.kind = 98; break;
case "const": t.kind = 21; break;
case "unique": t.kind = 22; break;
case "extends": t.kind = 23; break;
diff --git a/float_test11.bpl b/float_test11.bpl
index cf9fd3a2..cee3e36e 100644
--- a/float_test11.bpl
+++ b/float_test11.bpl
@@ -1,38 +1,55 @@
//Translation from interpolation.c
//Should Verify
-//Returns inconclusize? What does that mean?
+//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 : float;
- var t : float;
- var min : [int] float;
- var max : [int] float;
+ var z : float32;
+ var t : float32;
+ var min : [int] float32;
+ var max : [int] float32;
- min[0] := fp(5);
- min[1] := fp(10);
- min[2] := fp(12);
- min[3] := fp(30);
- min[4] := fp(150);
+ 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] := fp(10);
- max[1] := fp(12);
- max[2] := fp(30);
- max[3] := fp(150);
- max[4] := fp(300);
+ 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;
- }
+ //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 >= fp(0) && z <= fp(1));
+ assert(z >= TO_FLOAT32_INT(0) && z <= TO_FLOAT32_INT(1));
} \ No newline at end of file
diff --git a/float_test13.bpl b/float_test13.bpl
index d073836d..e5402539 100644
--- a/float_test13.bpl
+++ b/float_test13.bpl
@@ -1,17 +1,19 @@
//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 : float;
- var y : float;
- var z : float;
+ var x : float32;
+ var y : float32;
+ var z : float32;
havoc x;
- assume(x >= fp(-1) && x <= fp(1));
+ assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1));
- if (x != fp(0)) {
+ if (x != TO_FLOAT32_INT(0)) {
y := x * x;
- assert(y != fp(0));
- z := fp(1) / y;
+ assert(y != TO_FLOAT32_INT(0));
+ z := TO_FLOAT32_INT(1) / y;
}
} \ No newline at end of file
diff --git a/float_test14.bpl b/float_test14.bpl
index 9b5dab0a..1505c361 100644
--- a/float_test14.bpl
+++ b/float_test14.bpl
@@ -1,17 +1,20 @@
-//Translation from inv_square_false-unreach-call.c
+//Translation from inv_square_true-unreach-call.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 : float;
- var y : float;
- var z : float;
+ var x : float32;
+ var y : float32;
+ var z : float32;
havoc x;
- assume(x >= fp(-1) && x <= fp(1));
+ assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1));
- if (x <= fp(-.00000000000000000001) || x >= fp(.00000000000000000001)) {
+ if (x <= TO_FLOAT32_REAL(-1e-20) || x >= TO_FLOAT32_REAL(1e-20)) {
y := x * x;
- assert(y != fp(0));
- z := fp(1) / y;
+ assert(y != TO_FLOAT32_INT(0));
+ z := TO_FLOAT32_INT(1) / y;
}
} \ No newline at end of file
diff --git a/float_test2.bpl b/float_test2.bpl
index da74909b..d78c339d 100644
--- a/float_test2.bpl
+++ b/float_test2.bpl
@@ -1,13 +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 : float;
- var y : float;
- var z : float;
- var r : float;
- x := fp(1000000);
- y := x + fp(1);
- z := x - fp(1);
+ 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 == fp(2);
+ assert r == TO_FLOAT32_INT(2);
} \ No newline at end of file
diff --git a/float_test3.bpl b/float_test3.bpl
index dd0c1ba4..67c6ba48 100644
--- a/float_test3.bpl
+++ b/float_test3.bpl
@@ -1,13 +1,13 @@
//Translation from addsub_float_inexact.c
//Should give an error
procedure main() returns () {
- var x : float;
- var y : float;
- var z : float;
- var r : float;
- x := fp(10000000);
- y := x + fp(1);
- z := x - fp(1);
+ 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(0);
+ assert r == fp<8, 24>(2bv32);
} \ No newline at end of file
diff --git a/float_test4.bpl b/float_test4.bpl
index a7aa8c4b..a31aa215 100644
--- a/float_test4.bpl
+++ b/float_test4.bpl
@@ -1,20 +1,32 @@
//Translation from drift_tenth.c
-//Should Verify
-//FAILS; note that it succeeds when tick == fp(.1)
+//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 : float;
- var time : float;
+ var tick : float32;
+ var time : float32;
var i: int;
- tick := fp(1)/fp(10);
- time := fp(0);
+ 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 == fp(1));
+ //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
diff --git a/float_test5.bpl b/float_test5.bpl
index ce5d2bc7..7536f8fd 100644
--- a/float_test5.bpl
+++ b/float_test5.bpl
@@ -1,15 +1,18 @@
//Translation from filter1.c
//Should Verify
+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 E0 : float(11 53);
- var E1 : float(11 53);
- var S : float(11 53);
+ var E0 : float64;
+ var E1 : float64;
+ var S : float64);
var i : int;
var rand : int;
- E1 := fp(0 11 53);
- S := fp(0 11 53);
+ E1 := TO_FLOAT64_INT(0);
+ S := TO_FLOAT64_INT(0);
i := 0;
while (i <= 1000000)
diff --git a/float_test8.bpl b/float_test8.bpl
index 995ed4fa..7e78e206 100644
--- a/float_test8.bpl
+++ b/float_test8.bpl
@@ -1,12 +1,16 @@
//Translation from float_double.c
//Should Verify
-//FAILS: I don't have this functionality yet...
+
+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 : float(11 53);
- var y : float;
+ var x : float64;
+ var y : float32;
- x := fp(100000000000000000001 11 53);
- y := x;
- assert(x != y);
+ 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 12:44:14 +0000