From eed63d900b802e5551bf3c31772c39d365e7fcec Mon Sep 17 00:00:00 2001 From: Dietrich Date: Sun, 26 Apr 2015 15:24:07 -0600 Subject: added float type to the set array in Parser --- Source/Core/Parser.cs | 48 ++++++++++++++++++++++++------------------------ Source/Core/Scanner.cs | 2 +- float_test2.bpl | 4 ++-- 3 files changed, 27 insertions(+), 27 deletions(-) diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 578b9e5f..9a664606 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(99); + } else SynErr(97); 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(100); + } else SynErr(98); if (retTyd == null) { // construct a dummy type for the case of syntax error retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int)); @@ -497,7 +497,7 @@ private class BvBounds : Expr { impl = new Implementation(x, x.val, typeParams, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors); - } else SynErr(101); + } else SynErr(99); proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); } @@ -610,7 +610,7 @@ private class BvBounds : Expr { ty = new UnresolvedTypeIdentifier (tok, tok.val, args); } else if (la.kind == 17 || la.kind == 19) { MapType(out ty); - } else SynErr(102); + } else SynErr(100); } void AttributesIdsTypeWhere(bool allowAttributes, bool allowWhereClauses, string context, System.Action action ) { @@ -677,7 +677,7 @@ private class BvBounds : Expr { Get(); Type(out ty); Expect(10); - } else SynErr(103); + } else SynErr(101); } void Ident(out IToken/*!*/ x) { @@ -707,7 +707,7 @@ private class BvBounds : Expr { } else if (la.kind == 17 || la.kind == 19) { MapType(out ty); ts.Add(ty); - } else SynErr(104); + } else SynErr(102); } void MapType(out Bpl.Type/*!*/ ty) { @@ -892,7 +892,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { SpecPrePost(true, pre, post); } else if (la.kind == 36 || la.kind == 37) { SpecPrePost(false, pre, post); - } else SynErr(105); + } else SynErr(103); } void ImplBody(out List/*!*/ locals, out StmtList/*!*/ stmtList) { @@ -924,7 +924,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Proposition(out e); Expect(8); post.Add(new Ensures(tok, free, e, null, kv)); - } else SynErr(106); + } else SynErr(104); } void StmtList(out StmtList/*!*/ stmtList) { @@ -1063,7 +1063,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { c = new YieldCmd(x); break; } - default: SynErr(107); break; + default: SynErr(105); break; } } @@ -1080,7 +1080,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } else if (la.kind == 45) { BreakCmd(out bcmd); ec = bcmd; - } else SynErr(108); + } else SynErr(106); } void TransferCmd(out TransferCmd/*!*/ tc) { @@ -1100,7 +1100,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } else if (la.kind == 39) { Get(); tc = new ReturnCmd(t); - } else SynErr(109); + } else SynErr(107); Expect(8); } @@ -1125,7 +1125,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Get(); StmtList(out els); elseOption = els; - } else SynErr(110); + } else SynErr(108); } ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); } @@ -1189,7 +1189,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } else if (StartOf(9)) { Expression(out ee); e = ee; - } else SynErr(111); + } else SynErr(109); Expect(10); } @@ -1236,7 +1236,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } Expect(8); c = new AssignCmd(x, lhss, rhss); - } else SynErr(112); + } else SynErr(110); } void CallCmd(out Cmd c) { @@ -1353,7 +1353,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } Expect(10); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; - } else SynErr(113); + } else SynErr(111); } void Expressions(out List/*!*/ es) { @@ -1398,7 +1398,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Get(); } else if (la.kind == 56) { Get(); - } else SynErr(114); + } else SynErr(112); } void LogicalExpression(out Expr/*!*/ e0) { @@ -1436,7 +1436,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Get(); } else if (la.kind == 58) { Get(); - } else SynErr(115); + } else SynErr(113); } void ExpliesOp() { @@ -1444,7 +1444,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Get(); } else if (la.kind == 60) { Get(); - } else SynErr(116); + } else SynErr(114); } void RelationalExpression(out Expr/*!*/ e0) { @@ -1462,7 +1462,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Get(); } else if (la.kind == 62) { Get(); - } else SynErr(117); + } else SynErr(115); } void OrOp() { @@ -1470,7 +1470,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Get(); } else if (la.kind == 64) { Get(); - } else SynErr(118); + } else SynErr(116); } void BvTerm(out Expr/*!*/ e0) { @@ -1537,7 +1537,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { x = t; op=BinaryOperator.Opcode.Ge; break; } - default: SynErr(119); break; + default: SynErr(117); break; } } @@ -1569,7 +1569,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } else if (la.kind == 75) { Get(); x = t; op=BinaryOperator.Opcode.Sub; - } else SynErr(120); + } else SynErr(118); } void Power(out Expr/*!*/ e0) { @@ -1597,7 +1597,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } else if (la.kind == 78) { Get(); x = t; op=BinaryOperator.Opcode.RealDiv; - } else SynErr(121); + } else SynErr(119); } void UnaryExpression(out Expr/*!*/ e) { @@ -1616,7 +1616,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); } else if (StartOf(14)) { CoercionExpression(out e); - } else SynErr(122); + } else SynErr(120); } void NegOp() { diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index 9ac26b7b..c41d0a9e 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -508,7 +508,7 @@ public class Scanner { case "int": t.kind = 14; break; case "real": t.kind = 15; break; case "bool": t.kind = 16; break; - case "float": t.kind = 136; break; + case "float": 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/float_test2.bpl b/float_test2.bpl index fa34d8cf..71ea7dee 100644 --- a/float_test2.bpl +++ b/float_test2.bpl @@ -1,5 +1,5 @@ procedure F() returns () { - var x : float; - var y : float; + var x : real; + var y : real; assert x == y; } \ No newline at end of file -- cgit v1.2.3