From 6fad4313b1a4e7f8e6cfcd12b92126a3d9ad58d0 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 4 Jan 2016 19:26:36 -0800 Subject: Added several test cases and some basic documentation for fp usage --- Source/AbsInt/IntervalDomain.cs | 29 ++++++++++++-- Source/Basetypes/BigFloat.cs | 30 +++++++++----- Source/BoogieDriver/BoogieDriver.cs | 2 +- float_test.bpl | 16 ++++++-- float_test10.bpl | 21 ++++++++-- float_test11.bpl | 38 ++++++++++++++++++ float_test12.bpl | 43 ++++++++++++++++++++ float_test13.bpl | 17 ++++++++ float_test14.bpl | 17 ++++++++ float_test15.bpl | 24 +++++++++++ float_test16.bpl | 8 ++++ float_test17.bpl | 11 ++++++ float_test18.bpl | 36 +++++++++++++++++ float_test19.bpl | 36 +++++++++++++++++ float_test2.bpl | 16 ++++++-- float_test20.bpl | 14 +++++++ float_test3.bpl | 14 ++++++- float_test4.bpl | 23 +++++++++-- float_test5.bpl | 35 ++++++++++++++-- float_test6.bpl | 43 ++++++++++++++++++-- float_test7.bpl | 41 +++++++++++++++++-- float_test8.bpl | 13 +++++- float_test9.bpl | 37 +++++++++++++++-- fp_documentation.txt | 79 +++++++++++++++++++++++++++++++++++++ 24 files changed, 596 insertions(+), 47 deletions(-) create mode 100644 float_test11.bpl create mode 100644 float_test12.bpl create mode 100644 float_test13.bpl create mode 100644 float_test14.bpl create mode 100644 float_test15.bpl create mode 100644 float_test16.bpl create mode 100644 float_test17.bpl create mode 100644 float_test18.bpl create mode 100644 float_test19.bpl create mode 100644 float_test20.bpl create mode 100644 fp_documentation.txt 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 -- cgit v1.2.3