summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/AbsInt/IntervalDomain.cs2
-rw-r--r--Source/Basetypes/BigFloat.cs56
-rw-r--r--Source/Core/Parser.cs33
-rw-r--r--float_test4.bpl5
-rw-r--r--float_test5.bpl5
-rw-r--r--float_test6.bpl5
6 files changed, 61 insertions, 45 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 502b7075..a27ae68d 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -673,7 +673,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
Hi = ceiling;
} else if (node.Val is BigFloat) {
BigInteger floor, ceiling;
- ((BigDec)node.Val).FloorCeiling(out floor, out ceiling);
+ ((BigFloat)node.Val).FloorCeiling(out floor, out ceiling);
Lo = floor;
Hi = ceiling;
} else if (node.Val is bool) {
diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index 7c8b6001..d93f7d7b 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -88,40 +88,27 @@ namespace Microsoft.Basetypes
[Pure]
public static BigFloat FromString(string v) {
- if (v == null) throw new FormatException();
-
- BIM integral = BIM.Zero;
- BIM fraction = BIM.Zero;
- int exponent = 0;
-
- int len = v.Length;
-
- int i = v.IndexOf('e');
- if (i >= 0) {
- if (i + 1 == v.Length) throw new FormatException();
- exponent = Int32.Parse(v.Substring(i + 1, len - i - 1));
- len = i;
- }
-
- int fractionLen = 0;
- i = v.IndexOf('.');
- if (i >= 0) {
- if (i + 1 == v.Length) throw new FormatException();
- fractionLen = len - i - 1;
- fraction = BIM.Parse(v.Substring(i + 1, fractionLen));
- len = i;
- }
-
- integral = BIM.Parse(v.Substring(0, len));
-
- if (!fraction.IsZero) {
- while (fractionLen > 0) {
- integral = integral * two;
- exponent = exponent - 1;
- fractionLen = fractionLen - 1;
+ String[] vals = v.Split(' ');
+ if (vals.Length == 0 || vals.Length > 4)
+ throw new FormatException();
+ try
+ {
+ switch (vals.Length) {
+ case 1:
+ return Round(decimal.Parse(vals[0]), 23, 8);
+ case 2:
+ return new BigFloat(BIM.Parse(vals[0]), Int32.Parse(vals[1]), 23, 8);
+ case 3:
+ return Round(decimal.Parse(vals[0]), Int32.Parse(vals[1]), Int32.Parse(vals[2]));
+ case 4:
+ return new BigFloat(BIM.Parse(vals[0]), Int32.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3]));
+ default:
+ throw new FormatException(); //Unreachable
}
}
- return new BigFloat(integral - fraction, exponent, 23, 8);
+ catch (Exception) { //Catch parsing errors
+ throw new FormatException();
+ }
}
internal BigFloat(BIM mantissa, int exponent, int mantissaSize, int exponentSize) {
@@ -166,6 +153,11 @@ namespace Microsoft.Basetypes
////////////////////////////////////////////////////////////////////////////
// Conversion operations
+ public static BigFloat Round(decimal d, int mantissaSize, int exponentSize)
+ { //TODO: round the given decimal to the nearest fp value
+ return new BigFloat(0, 0, mantissaSize, exponentSize);
+ }
+
// ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
/// <summary>
/// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index b333f654..7335dd37 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -1879,15 +1879,29 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
{
//To be modified
string s = "";
- if (la.kind == 97) {
- Get();
- s = t.val;
- } else SynErr(128);
- try {
- n = BigFloat.FromString(s);
- } catch (FormatException) {
+ try
+ {
+ if (la.kind == 97)
+ {
+ //Expected format = fp (a b) || fp (a b c d)
+ Get(); //Skip the fp token
+ Get();
+ if (t.val != "(") { throw new FormatException(); }
+ while (la.kind == 3 || la.kind == 6) { //Get values between the parens
+ Get();
+ s += t.val + " ";
+ }
+ Get();
+ if (t.val != ")") { throw new FormatException(); }
+ }
+ else SynErr(137);
+
+ n = BigFloat.FromString(s.Trim());
+ }
+ catch (FormatException)
+ {
this.SemErr("incorrectly formatted floating point");
- n = BigFloat.ZERO;
+ n = BigFloat.ZERO;
}
}
@@ -2131,7 +2145,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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, 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,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,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,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,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,T,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,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, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,T,T,T, T,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}
@@ -2301,6 +2315,7 @@ public class Errors {
case 134: s = "invalid AttributeOrTrigger"; break;
case 135: s = "invalid AttributeParameter"; break;
case 136: s = "invalid QSep"; break;
+ case 137: s = "invalid Float"; break;
default: s = "error " + n; break;
}
diff --git a/float_test4.bpl b/float_test4.bpl
index a962713b..2388a281 100644
--- a/float_test4.bpl
+++ b/float_test4.bpl
@@ -1,6 +1,5 @@
procedure F() returns () {
var x : float;
- var y : float;
- y := x - x;
- assert y == fp (0,0,23,8);
+ x := fp (0 0);
+ assert x == fp (0 0 23 8);
} \ No newline at end of file
diff --git a/float_test5.bpl b/float_test5.bpl
new file mode 100644
index 00000000..b91e53e9
--- /dev/null
+++ b/float_test5.bpl
@@ -0,0 +1,5 @@
+ procedure F() returns () {
+ var x : float;
+ x := fp (0 0);
+ assert x == fp (1 0 23 8);
+} \ No newline at end of file
diff --git a/float_test6.bpl b/float_test6.bpl
new file mode 100644
index 00000000..532798d6
--- /dev/null
+++ b/float_test6.bpl
@@ -0,0 +1,5 @@
+ procedure F() returns () {
+ var x : float;
+ x := fp (1.5);
+ assert x == fp (1 0 23 8);
+} \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 13:51:25 +0000