Initial round of testing works with new syntax. Fixed an error where floating points could not be given as a function argument

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