From 51b7e8146f413b83a412572fcc9e3a1a8b302b79 Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Thu, 17 Mar 2016 13:01:10 -0600
Subject: modified floating point syntax and modified floating point constants
 to use bitvector values

---
 Source/Core/AbsyExpr.cs |  4 ++--
 Source/Core/Parser.cs   | 46 +++++++++++++++++++++++++++-------------------
 2 files changed, 29 insertions(+), 21 deletions(-)

(limited to 'Source/Core')

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index ad537288..6b2e1201 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -561,7 +561,7 @@ namespace Microsoft.Boogie {
     {
       Contract.Requires(tok != null);
       Val = v;
-      Type = Type.GetFloatType(v.ExponentSize, v.MantissaSize);
+      Type = Type.GetFloatType(v.ExponentSize, v.SignificandSize);
       if (immutable)
         CachedHashCode = ComputeHashCode();
     }
@@ -639,7 +639,7 @@ namespace Microsoft.Boogie {
           return Type.Real;
         } else if (Val is BigFloat) {
           BigFloat temp = (BigFloat)Val;
-          return Type.GetFloatType(temp.ExponentSize, temp.MantissaSize);
+          return Type.GetFloatType(temp.ExponentSize, temp.SignificandSize);
         } else if (Val is BvConst) {
           return Type.GetBvType(((BvConst)Val).Bits);
         } else {
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index bf35ccbe..77100d1c 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -669,7 +669,7 @@ private class BvBounds : Expr {
   } else if (la.kind == 98) {
    Get();
    if (la.kind == 3) {
-    Expect(3);
+     Get();
     switch (Int32.Parse(t.val)) {
     case 16:
         ty = new FloatType(t, 5, 11);
@@ -689,13 +689,14 @@ private class BvBounds : Expr {
     }
    }
    else {
-    Expect(19);
+    Expect(19); //<
     Expect(3);
     int exp = Int32.Parse(t.val);
+    Expect(12); //,
     Expect(3);
     int man = Int32.Parse(t.val);
     ty = new FloatType(t, exp, man);
-    Expect(20);
+    Expect(20); //>
    }
   } else if (la.kind == 16) {
 			Get();
@@ -1909,32 +1910,39 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
    {
      if (la.kind == 97) {
        bool negative = false;
-       int exp, sig;
+       int exp, sig, size;
        BigNum exp_val, sig_val, value;
-       //Expected format = fp(sign exp_val sig_val) || fp<exp sig>(value)
-       Get(); //Skip the fp token
-       Get();
-       if (t.val == "(") {
+       //Expected format = float(sign exp_val sig_val) || float<exp sig>(value)
+       Get(); //Skip the float token
+       if (la.val == "(") {
          Get();
+         Expect(16); //bool
          negative = Boolean.Parse(t.val);
+         Expect(12); //,
          BvLit(out exp_val, out exp);
+         Expect(12);
          BvLit(out sig_val, out sig);
          n = new BigFloat(negative, exp_val, sig_val, exp, sig);
+         Expect(10); //)
        }
-       else if (t.val == "<") {
-         Expect(14);
+       else if (la.val == "<") {
+         Get();
+         Expect(3);
          exp = Int32.Parse(t.val);
-         Expect(14);
+         Expect(12);
+         Expect(3);
          sig = Int32.Parse(t.val);
-         int size;
-         BvLit(out value, out size);
-         if (size != exp + sig)
-         {
-           this.SemErr("The given bitvector size of " + size + "does not match the provided floating-point size of " + (exp + sig));
-           n = BigFloat.ZERO(8, 24);
-           return;
+         Expect(20); //>
+         Expect(9); //(
+         if (la.kind == 4) {
+           Get();
+           n = new BigFloat(t.val, exp, sig);
+         }
+         else {
+           BvLit(out value, out size);
+           n = new BigFloat(value.ToString(), exp, sig);
          }
-         n = new BigFloat(t.val, exp, sig);
+         Expect(10); //)
        }
        else {
          throw new FormatException();
-- 
cgit v1.2.3