diff options
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/AbsyType.cs | 22 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 4 |
2 files changed, 14 insertions, 12 deletions
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 50fde975..5d41a8dd 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -330,20 +330,22 @@ namespace Microsoft.Boogie { return false;
}
}
- public virtual int FloatMantissa {
- get {
+ public virtual int FloatExponent
+ {
+ get
+ {
{
Contract.Assert(false);
throw new cce.UnreachableException();
- } // Type.FloatMantissa should never be called
+ } // Type.FloatExponent should never be called
}
}
- public virtual int FloatExponent {
+ public virtual int FloatMantissa {
get {
{
Contract.Assert(false);
throw new cce.UnreachableException();
- } // Type.FloatExponent should never be called
+ } // Type.FloatMantissa should never be called
}
}
public virtual bool IsBv {
@@ -1050,14 +1052,14 @@ namespace Microsoft.Boogie { public FloatType(IToken token, int exponent, int mantissa)
: base(token) {
Contract.Requires(token != null);
- Mantissa = mantissa;
Exponent = exponent;
+ Mantissa = mantissa;
}
public FloatType(int exponent, int mantissa)
: base(Token.NoToken) {
- Mantissa = mantissa;
Exponent = exponent;
+ Mantissa = mantissa;
}
//----------- Cloning ----------------------------------
@@ -1092,7 +1094,7 @@ namespace Microsoft.Boogie { public override string ToString()
{
Contract.Ensures(Contract.Result<string>() != null);
- return "(_ FP " + Exponent + " " + Mantissa + ")";
+ return "float (" + Exponent + " " + Mantissa + ")";
}
//----------- Equality ----------------------------------
@@ -1119,10 +1121,10 @@ namespace Microsoft.Boogie { //Contract.Requires(cce.NonNullElements(unifier));
that = that.Expanded;
if (that is TypeProxy || that is TypeVariable) {
- return that.Unify(this, unifiableVariables, unifier);
+ return that.Unify(this, unifiableVariables, unifier);
}
else {
- return this.Equals(that);
+ return this.Equals(that);
}
}
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index bb372cfb..2550c334 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -366,7 +366,7 @@ private class BvBounds : Expr { Get();
Type(out retTy);
retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy);
- } else SynErr(97);
+ } else SynErr(99);
if (la.kind == 27) {
Get();
Expression(out tmp);
@@ -374,7 +374,7 @@ private class BvBounds : Expr { Expect(28);
} else if (la.kind == 8) {
Get();
- } else SynErr(98);
+ } else SynErr(100);
if (retTyd == null) {
// construct a dummy type for the case of syntax error
retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int));
|