summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core')
-rw-r--r--Source/Core/AbsyType.cs214
-rw-r--r--Source/Core/Core.csproj2
-rw-r--r--Source/Core/Parser.cs283
-rw-r--r--Source/Core/Scanner.cs2
-rw-r--r--Source/Core/StandardVisitor.cs6
5 files changed, 428 insertions, 79 deletions
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 2953f15e..96de5c0b 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -244,6 +244,11 @@ namespace Microsoft.Boogie {
return false;
}
}
+ public virtual bool IsFloat {
+ get {
+ return false;
+ }
+ }
public virtual bool IsBool {
get {
return false;
@@ -320,6 +325,29 @@ namespace Microsoft.Boogie {
}
}
+ public virtual bool isFloat {
+ get {
+ return false;
+ }
+ }
+ public virtual int FloatExponent
+ {
+ get
+ {
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // Type.FloatExponent should never be called
+ }
+ }
+ public virtual int FloatMantissa {
+ get {
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // Type.FloatMantissa should never be called
+ }
+ }
public virtual bool IsBv {
get {
return false;
@@ -358,6 +386,14 @@ namespace Microsoft.Boogie {
}
}
+ static public FloatType GetFloatType(int exp, int man) {
+ Contract.Requires(0 <= exp);
+ Contract.Requires(0 <= man);
+ Contract.Ensures(Contract.Result<FloatType>() != null);
+
+ return new FloatType(exp, man);
+ }
+
//------------ Match formal argument types on actual argument types
//------------ and return the resulting substitution of type variables
@@ -1008,6 +1044,165 @@ namespace Microsoft.Boogie {
//=====================================================================
+ //Note that the functions in this class were directly copied from the BV class just below
+ public class FloatType : Type {
+ public readonly int Mantissa; //Size of mantissa in bits
+ public readonly int Exponent; //Size of exponent in bits
+
+ public FloatType(IToken token, int exponent, int mantissa)
+ : base(token) {
+ Contract.Requires(token != null);
+ Exponent = exponent;
+ Mantissa = mantissa;
+ }
+
+ public FloatType(int exponent, int mantissa)
+ : base(Token.NoToken) {
+ Exponent = exponent;
+ Mantissa = mantissa;
+ }
+
+ //----------- Cloning ----------------------------------
+ // We implement our own clone-method, because bound type variables
+ // have to be created in the right way. It is /not/ ok to just clone
+ // everything recursively.
+
+ public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap)
+ {
+ //Contract.Requires(cce.NonNullElements(varMap));
+ Contract.Ensures(Contract.Result<Type>() != null);
+ // FloatTypes are immutable anyway, we do not clone
+ return this;
+ }
+
+ public override Type CloneUnresolved()
+ {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return this;
+ }
+
+ //----------- Linearisation ----------------------------------
+
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength)
+ {
+ //Contract.Requires(stream != null);
+ // no parentheses are necessary for bitvector-types
+ stream.SetToken(this);
+ stream.Write("{0}", this);
+ }
+
+ public override string ToString()
+ {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return "float (" + Exponent + " " + Mantissa + ")";
+ }
+
+ //----------- Equality ----------------------------------
+
+ [Pure]
+ public override bool Equals(Type/*!*/ that,
+ List<TypeVariable>/*!*/ thisBoundVariables,
+ List<TypeVariable>/*!*/ thatBoundVariables)
+ {
+ FloatType thatFloatType = TypeProxy.FollowProxy(that.Expanded) as FloatType;
+ return thatFloatType != null && this.Mantissa == thatFloatType.Mantissa && this.Exponent == thatFloatType.Exponent;
+ }
+
+ //----------- Unification of types -----------
+
+ public override bool Unify(Type/*!*/ that,
+ List<TypeVariable>/*!*/ unifiableVariables,
+ // an idempotent substitution that describes the
+ // unification result up to a certain point
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier)
+ {
+ //Contract.Requires(that != null);
+ //Contract.Requires(unifiableVariables != null);
+ //Contract.Requires(cce.NonNullElements(unifier));
+ that = that.Expanded;
+ if (that is TypeProxy || that is TypeVariable) {
+ return that.Unify(this, unifiableVariables, unifier);
+ }
+ else {
+ return this.Equals(that);
+ }
+ }
+
+ //----------- Substitution of free variables with types not containing bound variables -----------------
+
+ public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst)
+ {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return this;
+ }
+
+ //----------- Hashcodes ----------------------------------
+
+ [Pure]
+ public override int GetHashCode(List<TypeVariable> boundVariables)
+ {
+ return this.Mantissa.GetHashCode() + this.Exponent.GetHashCode();
+ }
+
+ //----------- Resolution ----------------------------------
+
+ public override Type ResolveType(ResolutionContext rc)
+ {
+ //Contract.Requires(rc != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ // nothing to resolve
+ return this;
+ }
+
+ // determine the free variables in a type, in the order in which the variables occur
+ public override List<TypeVariable>/*!*/ FreeVariables
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);
+
+ return new List<TypeVariable>(); // bitvector-type are closed
+ }
+ }
+
+ public override List<TypeProxy/*!*/>/*!*/ FreeProxies
+ {
+ get
+ {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>()));
+ return new List<TypeProxy/*!*/>();
+ }
+ }
+
+ //----------- Getters/Issers ----------------------------------
+
+ public override bool IsFloat {
+ get {
+ return true;
+ }
+ }
+ public override int FloatMantissa {
+ get {
+ return Mantissa;
+ }
+ }
+ public override int FloatExponent {
+ get {
+ return Exponent;
+ }
+ }
+
+ public override Absy StdDispatch(StandardVisitor visitor)
+ {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
+ return visitor.VisitFloatType(this);
+ }
+
+ }
+
+ //=====================================================================
+
public class BvType : Type {
public readonly int Bits;
@@ -1899,6 +2094,12 @@ Contract.Requires(that != null);
return p != null && p.IsReal;
}
}
+ public override bool IsFloat {
+ get {
+ Type p = ProxyFor;
+ return p != null && p.IsFloat;
+ }
+ }
public override bool IsBool {
get {
Type p = ProxyFor;
@@ -2747,11 +2948,20 @@ Contract.Requires(that != null);
return ExpandedType.IsInt;
}
}
- public override bool IsReal {
- get {
+ public override bool IsReal
+ {
+ get
+ {
return ExpandedType.IsReal;
}
}
+ public override bool IsFloat
+ {
+ get
+ {
+ return ExpandedType.IsFloat;
+ }
+ }
public override bool IsBool {
get {
return ExpandedType.IsBool;
diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index af525fab..7c4cb7ae 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -186,7 +186,7 @@
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\Basetypes\Basetypes.csproj">
- <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
+ <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>
<Name>Basetypes</Name>
</ProjectReference>
<ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 793bb96e..1f8d17d6 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -24,7 +24,8 @@ public class Parser {
public const int _string = 4;
public const int _decimal = 5;
public const int _float = 6;
- public const int maxT = 96;
+ public const int _fp = 97;
+ public const int maxT = 98;
const bool T = true;
const bool x = false;
@@ -365,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);
@@ -373,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));
@@ -664,8 +665,11 @@ private class BvBounds : Expr {
ty = new BasicType(t, SimpleType.Int);
} else if (la.kind == 15) {
Get();
- ty = new BasicType(t, SimpleType.Real);
- } else if (la.kind == 16) {
+ ty = new BasicType(t, SimpleType.Real);
+ } else if (la.kind == 98) {
+ Get();
+ ty = FType();
+ } else if (la.kind == 16) {
Get();
ty = new BasicType(t, SimpleType.Bool);
} else if (la.kind == 9) {
@@ -675,6 +679,39 @@ private class BvBounds : Expr {
} else SynErr(101);
}
+ FloatType FType() {
+ if (t.val.Length > 5) {
+ switch (Int32.Parse(t.val.Substring(5))) {
+ case 16:
+ return new FloatType(t, 5, 11);
+ case 32:
+ return new FloatType(t, 8, 24);
+ case 64:
+ return new FloatType(t, 11, 53);
+ case 128:
+ return new FloatType(t, 15, 113);
+ default:
+ SynErr(3);
+ return new FloatType(t, 0, 0);
+ }
+ }
+ else {
+ try {
+ Expect(19); //<
+ Expect(3); //int
+ int exp = Int32.Parse(t.val);
+ Expect(12); //,
+ Expect(3); //int
+ int man = Int32.Parse(t.val);
+ Expect(20); //>
+ return new FloatType(t, exp, man);
+ }
+ catch (Exception) {
+ return new FloatType(t, 0, 0);
+ }
+ }
+ }
+
void Ident(out IToken/*!*/ x) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null);
Expect(1);
@@ -1619,7 +1656,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Get();
} else if (la.kind == 81) {
Get();
- } else SynErr(121);
+ } else SynErr(123);
}
void CoercionExpression(out Expr/*!*/ e) {
@@ -1643,7 +1680,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
}
- } else SynErr(122);
+ } else SynErr(124);
}
}
@@ -1714,7 +1751,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
void AtomExpression(out Expr/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd;
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; BigFloat fp;
List<Expr>/*!*/ es; List<Variable>/*!*/ ds; Trigger trig;
List<TypeVariable>/*!*/ typeParams;
IdentifierExpr/*!*/ id;
@@ -1739,11 +1776,16 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
e = new LiteralExpr(t, bn);
break;
}
- case 5: case 6: {
+ case 5: case 6: {
Dec(out bd);
e = new LiteralExpr(t, bd);
break;
}
+ case 97: {
+ Float(out fp);
+ e = new LiteralExpr(t, fp);
+ break;
+ }
case 2: {
BvLit(out bn, out n);
e = new LiteralExpr(t, bn, n);
@@ -1759,7 +1801,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
e = new NAryExpr(x, new FunctionCall(id), es);
} else if (la.kind == 10) {
e = new NAryExpr(x, new FunctionCall(id), new List<Expr>());
- } else SynErr(123);
+ } else SynErr(125);
Expect(10);
}
break;
@@ -1791,6 +1833,15 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e });
break;
}
+ case 98: {
+ Get();
+ x = t;
+ Expect(19);
+ Expression(out e);
+ Expect(20);
+ e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToFloat), new List<Expr> { e });
+ break;
+ }
case 9: {
Get();
if (StartOf(9)) {
@@ -1818,7 +1869,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
SemErr("triggers not allowed in lambda expressions");
if (typeParams.Count + ds.Count > 0)
e = new LambdaExpr(x, typeParams, ds, kv, e);
- } else SynErr(124);
+ } else SynErr(126);
Expect(10);
break;
}
@@ -1831,7 +1882,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
e = new CodeExpr(locals, blocks);
break;
}
- default: SynErr(125); break;
+ default: SynErr(127); break;
}
}
@@ -1843,7 +1894,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
} else if (la.kind == 6) {
Get();
s = t.val;
- } else SynErr(126);
+ } else SynErr(128);
try {
n = BigDec.FromString(s);
} catch (FormatException) {
@@ -1853,6 +1904,77 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
}
+ /// <summary>
+ /// Creates a floating point from the current token value
+ /// </summary>
+ /// <param name="n"></param>
+ void Float(out BigFloat n)
+ {
+ try
+ {
+ if (la.kind == 97) {
+ bool negative = false;
+ int exp, sig, size;
+ BigNum exp_val, sig_val, value;
+ //Expected format = float(sign exp_val sig_val) || float<exp sig>(value)
+ Get(); //Skip the float token
+ if (la.val == "(") {
+ Get();
+ if (la.val == "false")
+ negative = false;
+ else if (la.val == "true")
+ negative = true;
+ else
+ throw new FormatException();
+ Get();
+ 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 (la.val == "<") {
+ Get();
+ Expect(3);
+ exp = Int32.Parse(t.val);
+ Expect(12);
+ Expect(3);
+ sig = Int32.Parse(t.val);
+ Expect(20); //>
+ Expect(9); //(
+ if (la.kind == 1) { //NaN
+ Get();
+ n = new BigFloat(t.val, exp, sig);
+ }
+ else if (la.kind == 74 || la.kind == 75) { //+ or -
+ Get();
+ String s = t.val;
+ Get();
+ n = new BigFloat(s + t.val, exp, sig);
+ }
+ else {
+ BvLit(out value, out size);
+ n = new BigFloat(value.ToString(), exp, sig);
+ }
+ Expect(10); //)
+ }
+ else {
+ throw new FormatException();
+ }
+ }
+ else {
+ n = BigFloat.ZERO(8, 24);
+ SynErr(137);
+ }
+ }
+ catch (FormatException)
+ {
+ this.SemErr("incorrectly formatted floating point");
+ n = BigFloat.ZERO(8, 24);
+ }
+ }
+
void BvLit(out BigNum n, out int m) {
Expect(2);
int pos = t.val.IndexOf("bv");
@@ -1874,7 +1996,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
Get();
} else if (la.kind == 89) {
Get();
- } else SynErr(127);
+ } else SynErr(129);
}
void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds,
@@ -1892,7 +2014,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
}
} else if (la.kind == 1 || la.kind == 27) {
BoundVars(q, out ds);
- } else SynErr(128);
+ } else SynErr(130);
QSep();
while (la.kind == 27) {
AttributeOrTrigger(ref kv, ref trig);
@@ -1905,7 +2027,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Get();
} else if (la.kind == 91) {
Get();
- } else SynErr(129);
+ } else SynErr(131);
}
void Lambda() {
@@ -1913,7 +2035,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Get();
} else if (la.kind == 93) {
Get();
- } else SynErr(130);
+ } else SynErr(132);
}
void IfThenElseExpression(out Expr/*!*/ e) {
@@ -1983,7 +2105,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Get();
Expression(out e);
b = new Block(x,x.val,cs,new ReturnExprCmd(t,e));
- } else SynErr(131);
+ } else SynErr(133);
Expect(8);
}
@@ -2040,7 +2162,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
trig.AddLast(new Trigger(tok, true, es, null));
}
- } else SynErr(132);
+ } else SynErr(134);
Expect(28);
}
@@ -2055,7 +2177,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
} else if (StartOf(9)) {
Expression(out e);
o = e;
- } else SynErr(133);
+ } else SynErr(135);
}
void QSep() {
@@ -2063,7 +2185,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Get();
} else if (la.kind == 95) {
Get();
- } else SynErr(134);
+ } else SynErr(136);
}
@@ -2078,24 +2200,24 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Expect(0);
}
- static readonly bool[,]/*!*/ set = {
- {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, 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,T,x,x, x,T,x,x, x,T,T,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,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,T,x,x, x,x,T,T, T,T,x,T, 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,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,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,T,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,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,T,x,x, x,x,T,T, T,T,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,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,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,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, 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,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,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, 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,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,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,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,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, 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,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,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,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}
+ static readonly bool[,]/*!*/ set = { //grid is 17 x 100
+ {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, 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,T,x,x, x,T,x,x, x,T,T,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,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,T,x,x, x,x,T,T, T,T,x,T, 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,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,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, 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,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,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, x,x,x,x, x,x,x,x, x,x,T,x},
+ {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,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,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,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,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,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, 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,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,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, 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,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,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,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, 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,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}
};
} // end Parser
@@ -2117,6 +2239,12 @@ public class Errors {
count++;
}
+ /// <summary>
+ /// Returns a string corresponding to the syntax error of the given type
+ /// Note that many of these errors (0-98) correspond to token types (e.g. the la token)
+ /// </summary>
+ /// <param name="n"></param>
+ /// <returns></returns>
string GetSyntaxErrorString(int n) {
string s;
switch (n) {
@@ -2217,44 +2345,47 @@ public class Errors {
case 94: s = "\"::\" expected"; break;
case 95: s = "\"\\u2022\" expected"; break;
case 96: s = "??? expected"; break;
- case 97: s = "invalid Function"; break;
- case 98: s = "invalid Function"; break;
- case 99: s = "invalid Procedure"; break;
- case 100: s = "invalid Type"; break;
- case 101: s = "invalid TypeAtom"; break;
- case 102: s = "invalid TypeArgs"; break;
- case 103: s = "invalid Spec"; break;
- case 104: s = "invalid SpecPrePost"; break;
- case 105: s = "invalid LabelOrCmd"; break;
- case 106: s = "invalid StructuredCmd"; break;
- case 107: s = "invalid TransferCmd"; break;
- case 108: s = "invalid IfCmd"; break;
- case 109: s = "invalid Guard"; break;
- case 110: s = "invalid LabelOrAssign"; break;
- case 111: s = "invalid CallParams"; break;
- case 112: s = "invalid EquivOp"; break;
- case 113: s = "invalid ImpliesOp"; break;
- case 114: s = "invalid ExpliesOp"; break;
- case 115: s = "invalid AndOp"; break;
- case 116: s = "invalid OrOp"; break;
- case 117: s = "invalid RelOp"; break;
- case 118: s = "invalid AddOp"; break;
- case 119: s = "invalid MulOp"; break;
- case 120: s = "invalid UnaryExpression"; break;
- case 121: s = "invalid NegOp"; break;
- case 122: s = "invalid CoercionExpression"; break;
- case 123: s = "invalid AtomExpression"; break;
- case 124: s = "invalid AtomExpression"; break;
+ case 97: s = "fp expected"; break;
+ case 98: s = "\"float\" expected"; break;
+ case 99: s = "invalid Function"; break;
+ case 100: s = "invalid Function"; break;
+ case 101: s = "invalid Procedure"; break;
+ case 102: s = "invalid Type"; break;
+ case 103: s = "invalid TypeAtom"; break;
+ case 104: s = "invalid TypeArgs"; break;
+ case 105: s = "invalid Spec"; break;
+ case 106: s = "invalid SpecPrePost"; break;
+ case 107: s = "invalid LabelOrCmd"; break;
+ case 108: s = "invalid StructuredCmd"; break;
+ case 109: s = "invalid TransferCmd"; break;
+ case 110: s = "invalid IfCmd"; break;
+ case 111: s = "invalid Guard"; break;
+ case 112: s = "invalid LabelOrAssign"; break;
+ case 113: s = "invalid CallParams"; break;
+ case 114: s = "invalid EquivOp"; break;
+ case 115: s = "invalid ImpliesOp"; break;
+ case 116: s = "invalid ExpliesOp"; break;
+ case 117: s = "invalid AndOp"; break;
+ case 118: s = "invalid OrOp"; break;
+ case 119: s = "invalid RelOp"; break;
+ case 120: s = "invalid AddOp"; break;
+ case 121: s = "invalid MulOp"; break;
+ case 122: s = "invalid UnaryExpression"; break;
+ case 123: s = "invalid NegOp"; break;
+ case 124: s = "invalid CoercionExpression"; break;
case 125: s = "invalid AtomExpression"; break;
- case 126: s = "invalid Dec"; break;
- case 127: s = "invalid Forall"; break;
- case 128: s = "invalid QuantifierBody"; break;
- case 129: s = "invalid Exists"; break;
- case 130: s = "invalid Lambda"; break;
- case 131: s = "invalid SpecBlock"; break;
- case 132: s = "invalid AttributeOrTrigger"; break;
- case 133: s = "invalid AttributeParameter"; break;
- case 134: s = "invalid QSep"; break;
+ case 126: s = "invalid AtomExpression"; break;
+ case 127: s = "invalid AtomExpression"; break;
+ case 128: s = "invalid Dec"; break;
+ case 129: s = "invalid Forall"; break;
+ case 130: s = "invalid QuantifierBody"; break;
+ case 131: s = "invalid Exists"; break;
+ case 132: s = "invalid Lambda"; break;
+ case 133: s = "invalid SpecBlock"; break;
+ 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/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index e068fc4b..69023555 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -508,6 +508,8 @@ public class Scanner {
case "int": t.kind = 14; break;
case "real": t.kind = 15; break;
case "bool": t.kind = 16; break;
+ case "fp": t.kind = 97; break;
+ case "float": case "float16": case "float32": case "float64": case "float128": t.kind = 98; break;
case "const": t.kind = 21; break;
case "unique": t.kind = 22; break;
case "extends": t.kind = 23; break;
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index c845a589..c3d8a672 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -103,6 +103,12 @@ namespace Microsoft.Boogie {
Contract.Ensures(Contract.Result<Type>() != null);
return this.VisitType(node);
}
+ public virtual Type VisitFloatType(FloatType node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return this.VisitType(node);
+ }
public virtual Expr VisitBvConcatExpr(BvConcatExpr node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Expr>() != null);