Added several test cases and some basic documentation for fp usage

24 files changed, 596 insertions, 47 deletions

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index a27ae68d..0c954f9a 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -180,8 +180,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
             }

           }

           return e;

-        } else {

-          Contract.Assert(V.TypedIdent.Type.IsReal);

+        } else if (V.TypedIdent.Type.IsReal){

           Expr e = Expr.True;

           if (Lo != null && Hi != null && Lo == Hi) {

             // produce an equality

@@ -199,6 +198,30 @@ namespace Microsoft.Boogie.AbstractInterpretation
             }

           }

           return e;

+        } else {

+          Contract.Assert(V.TypedIdent.Type.IsFloat);

+          Expr e = Expr.True;

+          if (Lo != null && Hi != null && Lo == Hi)

+          {

+            // produce an equality

+            var ide = new IdentifierExpr(Token.NoToken, V);

+            e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type)));

+          }

+          else

+          {

+            // produce a (possibly empty) conjunction of inequalities

+            if (Lo != null)

+            {

+              var ide = new IdentifierExpr(Token.NoToken, V);

+              e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide));

+            }

+            if (Hi != null)

+            {

+              var ide = new IdentifierExpr(Token.NoToken, V);

+              e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type)));

+            }

+          }

+          return e;

         }

       }

     }

@@ -209,7 +232,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
       } else if (ty.IsReal) {

         return Expr.Literal(Basetypes.BigDec.FromBigInt(n));

       } else if (ty.IsFloat) {

-        return Expr.Literal(Basetypes.BigFloat.FromBigInt(n));

+        return Expr.Literal(Basetypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatMantissa));

       } else {

         Contract.Assume(ty.IsInt);

         return Expr.Literal(Basetypes.BigNum.FromBigInt(n));

diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index 6cf94feb..5b169263 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -92,16 +92,21 @@ namespace Microsoft.Basetypes
 

     [Pure]

     public static BigFloat FromInt(int v) {

-      return new BigFloat(v, 0, 24, 8);

+      return new BigFloat(v.ToString(), 8, 24);

     }

 

-    [Pure]

-    public static BigFloat FromLong(long v) {

-      return new BigFloat(0, v, 8, 24);

+    public static BigFloat FromInt(int v, int exponentSize, int mantissaSize)

+    {

+      return new BigFloat(v.ToString(), exponentSize, mantissaSize);

     }

 

     public static BigFloat FromBigInt(BIM v) {

-      return FromLong(Int64.Parse(v.ToString())); //Sketchy.  Hope this doesn't cause problems

+      return new BigFloat(v.ToString(), 8, 24);

+    }

+

+    public static BigFloat FromBigInt(BIM v, int exponentSize, int mantissaSize)

+    {

+      return new BigFloat(v.ToString(), exponentSize, mantissaSize);

     }

 

     public static BigFloat FromBigDec(BigDec v)

@@ -109,6 +114,11 @@ namespace Microsoft.Basetypes
       return new BigFloat(v.ToDecimalString(), 8, 24);

     }

 

+    public static BigFloat FromBigDec(BigDec v, int exponentSize, int mantissaSize)

+    {

+      return new BigFloat(v.ToDecimalString(), exponentSize, mantissaSize);

+    }

+

     [Pure]

     public static BigFloat FromString(string v) {

       String[] vals = v.Split(' ');

@@ -170,9 +180,9 @@ namespace Microsoft.Basetypes
         return;

       }

       //End special cases

-      if (this.dec_value.IndexOf(".") == -1)

+      if (this.dec_value.IndexOf('.') == -1 && this.dec_value.IndexOf('e') == -1)

         this.dec_value += ".0"; //Assures that the decimal value is a "real" number

-      if (this.dec_value.IndexOf(".") == 0)

+      if (this.dec_value.IndexOf('.') == 0)

         this.dec_value = "0" + this.dec_value; //Assures that decimals always have a 0 in front

     }

 

@@ -369,16 +379,18 @@ namespace Microsoft.Basetypes
 

     [Pure]

     public BigFloat Abs {

-      //TODO: fix for fp functionality

       get {

+        if (IsDec)

+          return dec_value[0] == '-' ? new BigFloat(dec_value.Remove(0, 1), ExponentSize, MantissaSize) : this;

         return new BigFloat(Exponent, Math.Abs(Mantissa), ExponentSize, MantissaSize);

       }

     }

 

     [Pure]

     public BigFloat Negate {

-      //TODO: Modify for correct fp functionality

       get {

+        if (IsDec)

+          return dec_value[0] == '-' ? new BigFloat(dec_value.Remove(0, 1), ExponentSize, MantissaSize) : new BigFloat("-" + dec_value, ExponentSize, MantissaSize);

         return new BigFloat(Exponent, -Mantissa, ExponentSize, MantissaSize);

       }

     }

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index cba74bc5..2345cc1e 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -90,7 +90,7 @@ namespace Microsoft.Boogie {
         }

       }

       ExecutionEngine.ProcessFiles(fileList);

-      return 0;

+        return 0;

 

     END:

       if (CommandLineOptions.Clo.XmlSink != null) {

diff --git a/float_test.bpl b/float_test.bpl
index ebd0ab47..fbf8e4e3 100644
--- a/float_test.bpl
+++ b/float_test.bpl
@@ -1,5 +1,13 @@
-procedure F(n: float) returns(r: float)
-	ensures r == n;
-{
-	r := n;
+//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(10000000 11 53);
+	y := x + fp(1 11 53);
+	z := x - fp(1 11 53);
+	r := y - z;
+	assert r == fp(2 11 53);
 }
\ No newline at end of file
diff --git a/float_test10.bpl b/float_test10.bpl
index 7423a3a0..566f7a56 100644
--- a/float_test10.bpl
+++ b/float_test10.bpl
@@ -1,5 +1,20 @@
- procedure F() returns () {
+//Translation from loop.c
+//Should return an error?  (The real case does as well...)
+
+procedure main() returns () {
 	var x : float;
-	x := fp (0.5 23 8);
-	assert x == fp (0 -1);
+	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/float_test11.bpl b/float_test11.bpl
new file mode 100644
index 00000000..cf9fd3a2
--- /dev/null
+++ b/float_test11.bpl
@@ -0,0 +1,38 @@
+//Translation from interpolation.c

+//Should Verify

+//Returns inconclusize?  What does that mean?

+

+procedure main() returns () {

+	var i : int;

+	var z : float;

+	var t : float;

+	var min : [int] float;

+	var max : [int] float;

+	

+	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/float_test12.bpl b/float_test12.bpl
new file mode 100644
index 00000000..c733b9f4
--- /dev/null
+++ b/float_test12.bpl
@@ -0,0 +1,43 @@
+//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/float_test13.bpl b/float_test13.bpl
new file mode 100644
index 00000000..d073836d
--- /dev/null
+++ b/float_test13.bpl
@@ -0,0 +1,17 @@
+//Translation from inv_square_false-unreach-call.c

+//Should return an error (without crashing)

+

+procedure main() returns () {

+	var x : float;

+	var y : float;

+	var z : float;

+	

+	havoc x;

+	assume(x >= fp(-1) && x <= fp(1));

+	

+	if (x != fp(0)) {

+		y := x * x;

+		assert(y != fp(0));

+		z := fp(1) / y;

+	}

+}
\ No newline at end of file
diff --git a/float_test14.bpl b/float_test14.bpl
new file mode 100644
index 00000000..9b5dab0a
--- /dev/null
+++ b/float_test14.bpl
@@ -0,0 +1,17 @@
+//Translation from inv_square_false-unreach-call.c

+//Should Verify

+

+procedure main() returns () {

+	var x : float;

+	var y : float;

+	var z : float;

+	

+	havoc x;

+	assume(x >= fp(-1) && x <= fp(1));

+	

+	if (x <= fp(-.00000000000000000001) || x >= fp(.00000000000000000001)) {

+		y := x * x;

+		assert(y != fp(0));

+		z := fp(1) / y;

+	}

+}
\ No newline at end of file
diff --git a/float_test15.bpl b/float_test15.bpl
new file mode 100644
index 00000000..1dc549ac
--- /dev/null
+++ b/float_test15.bpl
@@ -0,0 +1,24 @@
+//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/float_test16.bpl b/float_test16.bpl
new file mode 100644
index 00000000..69ae243d
--- /dev/null
+++ b/float_test16.bpl
@@ -0,0 +1,8 @@
+//Translation from nan_double_false-unreach-call.c

+//Should return an error

+

+procedure main() returns () {

+	var x : float(11 53);

+	havoc x;

+	assert(x==x);

+}
\ No newline at end of file
diff --git a/float_test17.bpl b/float_test17.bpl
new file mode 100644
index 00000000..caa1fa74
--- /dev/null
+++ b/float_test17.bpl
@@ -0,0 +1,11 @@
+//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/float_test18.bpl b/float_test18.bpl
new file mode 100644
index 00000000..71eb5286
--- /dev/null
+++ b/float_test18.bpl
@@ -0,0 +1,36 @@
+//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/float_test19.bpl b/float_test19.bpl
new file mode 100644
index 00000000..f00d8a2b
--- /dev/null
+++ b/float_test19.bpl
@@ -0,0 +1,36 @@
+//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/float_test2.bpl b/float_test2.bpl
index 956ac757..da74909b 100644
--- a/float_test2.bpl
+++ b/float_test2.bpl
@@ -1,5 +1,13 @@
-procedure F() returns () {
-	var x : float(11 53);
-	var y : float(11 53);
-	assert x == y;
+//Translation from addsub_float_exact.c
+//Should Verify
+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);
+	r := y - z;
+	assert r == fp(2);
 }
\ No newline at end of file
diff --git a/float_test20.bpl b/float_test20.bpl
new file mode 100644
index 00000000..57c605fd
--- /dev/null
+++ b/float_test20.bpl
@@ -0,0 +1,14 @@
+//Should return an error?

+//Translation from Rump_double.c

+

+procedure main() returns () {

+	var x : float(11 53);

+	var y : float(11 53);

+	var r : float(11 53);

+	

+	x := fp(77617 11 53);

+	y := fp(33096 11 53);

+	r := y*y*y*y*y*y * fp(333.75 11 53) + x*x * (x*x*y*y*fp(11 11 53) - y*y*y*y*y*y - y*y*y*y * fp(121 11 53) - fp(2 11 53)) + y*y*y*y*y*y*y*y * fp(5.5 11 53) + x / (y*fp(2 11 53));

+	

+	assert(r >= fp(0 11 53));

+}
\ No newline at end of file
diff --git a/float_test3.bpl b/float_test3.bpl
index e93e7df7..dd0c1ba4 100644
--- a/float_test3.bpl
+++ b/float_test3.bpl
@@ -1,3 +1,13 @@
- procedure F() returns () {
-	assert fp(5) == fp(5 8 23);
+//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);
+	r := y - z;
+	assert r == fp(0);
 }
\ No newline at end of file
diff --git a/float_test4.bpl b/float_test4.bpl
index 1252dc71..a7aa8c4b 100644
--- a/float_test4.bpl
+++ b/float_test4.bpl
@@ -1,5 +1,20 @@
- procedure F() returns () {
-	var x : float;
-	x := fp (.5 8 23);
-	assert x == fp (-1 0);
+//Translation from drift_tenth.c
+//Should Verify
+//FAILS; note that it succeeds when tick == fp(.1)
+
+procedure main() returns () {
+	var tick : float;
+	var time : float;
+	var i: int;
+	
+	tick := fp(1)/fp(10);
+	time := fp(0);
+	
+	i := 0;
+	while (i < 10)
+	{
+		time := time + tick;
+		i := i + 1;
+	}
+	assert(time == fp(1));
 }
\ No newline at end of file
diff --git a/float_test5.bpl b/float_test5.bpl
index be72b988..ce5d2bc7 100644
--- a/float_test5.bpl
+++ b/float_test5.bpl
@@ -1,4 +1,33 @@
-procedure F() returns () {
-	var x : float;
-	assert x - x == fp(0);
+//Translation from filter1.c
+//Should Verify
+
+procedure main() returns () {
+	var E0 : float(11 53);
+	var E1 : float(11 53);
+	var S : float(11 53);
+	var i : int;
+	var rand : int;
+	
+	E1 := fp(0 11 53);
+	S := fp(0 11 53);
+	
+	i := 0;
+	while (i <= 1000000)
+	{
+		havoc E0;
+		assume(E0 >= fp(-1 11 53) && E0 <= fp(1 11 53));
+		
+		havoc rand;
+		if (rand != 0) {
+			S := fp(0 11 53);
+		}
+		else {
+			S := fp(0.999 11 53) * S + E0 - E1;
+		}
+		E1 := E0;
+		
+		//assert(1==0);
+		assert(S >= fp(-1 11 53) && S <= fp(1 11 53));
+		i := i + 1;
+	}
 }
\ No newline at end of file
diff --git a/float_test6.bpl b/float_test6.bpl
index 423bc45a..6bef1137 100644
--- a/float_test6.bpl
+++ b/float_test6.bpl
@@ -1,5 +1,40 @@
-procedure F() returns () {
-	var x : float;
-	var y : float;
-	assert (x + x) + (y + y) == fp(0);
+//Translation from filter2.c
+//Should give an error
+//FAILS; doesn't generate terms!
+
+procedure main() returns () {
+	var E : float(11 53);
+	var E0 : float(11 53);
+	var E1 : float(11 53);
+	var S : float(11 53);
+	var S0 : float(11 53);
+	var S1 : float(11 53);
+	var i: int;
+	
+	havoc E;
+	havoc E0;
+	assume(E >= fp(0.0 11 53) && E <= fp(1.0 11 53));
+	assume(E0 >= fp(0.0 11 53) && E0 <= fp(1.0 11 53));
+	
+	E1 := fp(0.0 11 53);
+	S1 := fp(0.0 11 53);
+	S0 := fp(0.0 11 53);
+	S := fp(0.0 11 53);
+	
+	i := 0;
+//	while (i <= 1000000)
+//	{
+		E1 := E0;
+		E0 := E;
+	
+		havoc E;
+		assume(E >= fp(0.0 11 53) && E <= fp(1.0 11 53));
+		
+		S1 := S0;
+		S0 := S;
+		S := E*fp(0.7 11 53) - E0*fp(1.3 11 53) + E1*fp(1.1 11 53) + S0*fp(1.4 11 53) - S1*fp(0.7 11 53);
+		
+		assert(S >= fp(-4.0 11 53) && S <= fp(4.0 11 53));
+		//i := i + 1;
+//	}
 }
\ No newline at end of file
diff --git a/float_test7.bpl b/float_test7.bpl
index cc7a040b..8e07878d 100644
--- a/float_test7.bpl
+++ b/float_test7.bpl
@@ -1,5 +1,38 @@
-procedure F() returns () {
-	var x : float;
-	x := fp(.1) + fp(.1) + fp(.1);
-	assert x == fp(.3);
+//Translation from filter2.c
+//Should give an error
+//Same as the previous one; it works with reals!
+
+procedure main() returns () {
+	var E : real;
+	var E0 : real;
+	var E1 : real;
+	var S : real;
+	var S0 : real;
+	var S1 : real;
+	var i: int;
+	
+	havoc E;
+	havoc E0;
+	assume(E >= 0.0 && E <= 1.0);
+	assume(E0 >= 0.0 && E0 <= 1.0);
+	
+	S0 := 0.0;
+	S := 0.0;
+	
+	i := 0;
+	while (i <= 1000000)
+	{
+		E1 := E0;
+		E0 := E;
+		
+		havoc E;
+		assume(E >= 0.0 && E <= 1.0);
+		
+		S1 := S0;
+		S0 := S;
+		S := E*0.7 - E0*1.3 + E1*1.1 + S0*1.4 - S1*0.7;
+		
+		assert(S >= -4.0 && S <= 4.0);
+		i := i + 1;
+	}
 }
\ No newline at end of file
diff --git a/float_test8.bpl b/float_test8.bpl
index 554dcf00..995ed4fa 100644
--- a/float_test8.bpl
+++ b/float_test8.bpl
@@ -1,3 +1,12 @@
-procedure F() returns () {
-	assert fp(-oo)==fp(-oo);
+//Translation from float_double.c
+//Should Verify
+//FAILS: I don't have this functionality yet...
+
+procedure main() returns () {
+	var x : float(11 53);
+	var y : float;
+	
+	x := fp(100000000000000000001 11 53);
+	y := x;
+	assert(x != y);
 }
\ No newline at end of file
diff --git a/float_test9.bpl b/float_test9.bpl
index 7423a3a0..c3a42e6b 100644
--- a/float_test9.bpl
+++ b/float_test9.bpl
@@ -1,5 +1,34 @@
- procedure F() returns () {
-	var x : float;
-	x := fp (0.5 23 8);
-	assert x == fp (0 -1);
+//Translation from feedback_diverge.c
+//Should give an error
+//Not sure on this one...
+
+procedure main() returns () {
+	var A : float;
+	var B : float;
+	var X : float;
+	var i : int;
+	var rand : int;
+	
+	A := fp(0);
+	B := fp(0);
+	
+	i := 0;
+	while (i < 3600000) {
+		
+		havoc rand;
+		if (rand != 0) {
+			havoc X;
+			assume(X >= fp(-20) && X <= fp(20));
+		}
+		else {
+			X := B;
+		}
+		
+		B := B - (B * fp(2.0) - A - X) * fp(.005);
+		A := X;
+		
+		i := i + 1;
+	}
+	
+	assert(A >= fp(-100) && A <= fp(100));
 }
\ No newline at end of file
diff --git a/fp_documentation.txt b/fp_documentation.txt
new file mode 100644
index 00000000..09e60b9a
--- /dev/null
+++ b/fp_documentation.txt
@@ -0,0 +1,79 @@
+Floating Point Documentation for Boogie

+Written by Dietrich Geisler

+Contact: dgeisler50@gmail.com

+

+This document aims to describe the syntax for declaring and using floating points in Boogie

+

+--------------------------------------------------------------------------------

+Declaring Variables:

+

+The syntax for declaring a floating point variable is as follows:

+var name: float(exp man);

+Where exp is the size of the float exponent and man is the size of the float mantissa

+

+It is also acceptable to use the following syntax:

+var name: float();

+This syntax assumes the float exponent to be size 8 and the mantissa to be size 24

+

+example:

+var x: float(11 53)

+Declares a variable called x with a exponent sized 11 and mantissa sized 53

+

+--------------------------------------------------------------------------------

+Declaring Constants:

+

+All of the following syntax are viable for declaring a floating point constant:

+float(dec)

+float(exp_val man_val)

+float(dec exp man)

+float(exp_val man_val exp man)

+

+Where dec is the decimal value of the constant,

+exp_val/man_value are the integer values of their respective fields,

+And exp/man are the sizes of their respective fields.

+Note that when exp and man are not specified, they are given sizes 8 and 24 respectively

+

+--------------------------------------------------------------------------------

+Defined Operations:

+

+Given two floating point values x and y with the same size of exponent and mantissa

+The following operations operate as defined in Operators section of this document:

+http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml

+(Note that rounding mode is always assumed to be Round to Nearest Even (RNE))

+(Also note that operations not listed here are undefined)

+

+operatation		boogie syntax

+neg(x)			-x

+add(x, y)		x + y

+sub(x, y)		x - y

+mul(x, y)		x * y

+div(x, y)		x / y

+leq(x, y)		x <= y

+lt(x, y)		x < y

+geq(x, y)		x >= y

+gt(x, y)		x > y

+eq(x, y)		x == y

+

+--------------------------------------------------------------------------------

+Other:

+

+The following special values can be declared with the following syntax:

+Value		Declaration

+NaN			fp(nan exp man)

++oo			fp(oo exp man) OR fp(INF exp man)

+-oo			fp(-oo exp man) OR fp(INF exp man)

+-zero		fp(-zero exp man)

+Where exp and man are the sizes of the exponent and mantissa respectively

+

+--------------------------------------------------------------------------------

+Known Issues:

+

+There is currently no way to convert from a floating point to any other data type

+

+There is currently no way to convert the value of a variable to a floating point type

+For example, the following statements fails:

+var x : real;

+fp(x);

+

+Statements of the following form cause a parser error (parenthesis followed by fp constant)

+... (fp(1) + fp(1));
\ No newline at end of file