diff options
author | MichalMoskal <unknown> | 2009-12-17 01:17:59 +0000 |
---|---|---|
committer | MichalMoskal <unknown> | 2009-12-17 01:17:59 +0000 |
commit | 9447617aefbe9706b0d74a827181976e4b9e9d26 (patch) | |
tree | 471ea6938e90be46af5e6ce8e7ca88de1081c977 /Source | |
parent | fa8cb4c335668f180fa2c181ca6bb1ad87b54c4a (diff) |
Allow ":" in addition to "returns" in function definitions. Make the pretty-printer use ":" not "returns".
Allow foo(x,y,z:int,p,q:ptr) kind of syntax in function definitions.
Consequently foo(int,y:bool) is no longer allowed.
Update the testsuite to match that.
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Core/Absy.ssc | 16 | ||||
-rw-r--r-- | Source/Core/BoogiePL.atg | 49 | ||||
-rw-r--r-- | Source/Core/Parser.ssc | 266 | ||||
-rw-r--r-- | Source/Core/Scanner.ssc | 14 | ||||
-rw-r--r-- | Source/Core/parser.frame | 6 |
5 files changed, 226 insertions, 125 deletions
diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc index fd54412c..fc706e2c 100644 --- a/Source/Core/Absy.ssc +++ b/Source/Core/Absy.ssc @@ -1126,14 +1126,20 @@ namespace Microsoft.Boogie // base(that.tok, (!) that.Name);
}
- protected void EmitSignature (TokenTextWriter! stream)
+ protected void EmitSignature (TokenTextWriter! stream, bool shortRet)
{
Type.EmitOptionalTypeParams(stream, TypeParameters);
stream.Write("(");
InParams.Emit(stream);
stream.Write(")");
- if (OutParams.Length > 0)
+ if (shortRet)
+ {
+ assert OutParams.Length == 1;
+ stream.Write(" : ");
+ ((!)OutParams[0]).TypedIdent.Type.Emit(stream);
+ }
+ else if (OutParams.Length > 0)
{
stream.Write(" returns (");
OutParams.Emit(stream);
@@ -1262,7 +1268,7 @@ namespace Microsoft.Boogie } else {
stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(this.Name));
}
- EmitSignature(stream);
+ EmitSignature(stream, true);
if (Body != null) {
stream.WriteLine();
stream.WriteLine("{");
@@ -1539,7 +1545,7 @@ namespace Microsoft.Boogie stream.Write(this, level, "procedure ");
EmitAttributes(stream);
stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name));
- EmitSignature(stream);
+ EmitSignature(stream, false);
stream.WriteLine(";");
level++;
@@ -1751,7 +1757,7 @@ namespace Microsoft.Boogie stream.Write(this, level, "implementation ");
EmitAttributes(stream);
stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name));
- EmitSignature(stream);
+ EmitSignature(stream, false);
stream.WriteLine();
stream.WriteLine(level, "{0}", '{');
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 4fc91b35..eab10ff9 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -380,6 +380,8 @@ Function<out DeclarationSeq! ds> TypeVariableSeq! typeParams = new TypeVariableSeq();
VariableSeq arguments = new VariableSeq();
TypedIdent! tyd;
+ TypedIdent retTyd = null;
+ Type! retTy;
QKeyValue kv = null;
Expr definition = null;
Expr! tmp;
@@ -390,12 +392,51 @@ Function<out DeclarationSeq! ds> [ VarOrType<out tyd> (. arguments.Add(new Formal(tyd.tok, tyd, true)); .)
{ "," VarOrType<out tyd> (. arguments.Add(new Formal(tyd.tok, tyd, true)); .)
} ] ")"
- "returns" "(" VarOrType<out tyd> ")"
+ (
+ "returns" "(" VarOrType<out tyd> ")" (. retTyd = tyd; .)
+ |
+ ":" Type<out retTy> (. retTyd = new TypedIdent(retTy.tok, "", retTy); .)
+ )
( "{" Expression<out tmp> (. definition = tmp; .) "}" | ";" )
(.
+ if (retTyd == null) {
+ // construct a dummy type for the case of syntax error
+ tyd = new TypedIdent(token, "", new BasicType(token, SimpleType.Int));
+ } else {
+ tyd = retTyd;
+ }
Function! func = new Function(z, z.val, typeParams, arguments,
new Formal(tyd.tok, tyd, false), null, kv);
ds.Add(func);
+ bool allUnnamed = true;
+ foreach (Formal! f in arguments) {
+ if (f.TypedIdent.Name != "") {
+ allUnnamed = false;
+ break;
+ }
+ }
+ if (!allUnnamed) {
+ Type prevType = null;
+ for (int i = arguments.Length - 1; i >= 0; i--) {
+ TypedIdent! curr = ((!)arguments[i]).TypedIdent;
+ if (curr.Name == "") {
+ if (prevType == null) {
+ SemErr(curr.tok, "the type of the last parameter is unspecified");
+ break;
+ }
+ Type ty = curr.Type;
+ if (ty is UnresolvedTypeIdentifier &&
+ ((!)(ty as UnresolvedTypeIdentifier)).Arguments.Length == 0) {
+ curr.Name = ((!)(ty as UnresolvedTypeIdentifier)).Name;
+ curr.Type = prevType;
+ } else {
+ SemErr(curr.tok, "expecting an identifier as parameter name");
+ }
+ } else {
+ prevType = curr.Type;
+ }
+ }
+ }
if (definition != null) {
// generate either an axiom or a function body
if (QKeyValue.FindBoolAttribute(kv, "inline")) {
@@ -1199,9 +1240,9 @@ ArrayExpression<out Expr! e> (. if (store)
e = new NAryExpr(x, new MapStore(x, allArgs.Length - 2), allArgs);
else if (bvExtract)
- e = new ExtractExpr(x, e,
- ((BvBounds)index0).Upper.ToIntSafe,
- ((BvBounds)index0).Lower.ToIntSafe);
+ e = new BvExtractExpr(x, e,
+ ((BvBounds)index0).Upper.ToIntSafe,
+ ((BvBounds)index0).Lower.ToIntSafe);
else
e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs);
.)
diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc index 8ae741ab..a7453d09 100644 --- a/Source/Core/Parser.ssc +++ b/Source/Core/Parser.ssc @@ -118,6 +118,10 @@ private class BvBounds : Expr { errDist = 0;
}
+ public static void SemErr(IToken! tok, string! msg) {
+ Errors.SemErr(tok.filename, tok.line, tok.col, msg);
+ }
+
static void Get() {
for (;;) {
token = t;
@@ -260,6 +264,8 @@ private class BvBounds : Expr { TypeVariableSeq! typeParams = new TypeVariableSeq();
VariableSeq arguments = new VariableSeq();
TypedIdent! tyd;
+ TypedIdent retTyd = null;
+ Type! retTy;
QKeyValue kv = null;
Expr definition = null;
Expr! tmp;
@@ -283,10 +289,17 @@ private class BvBounds : Expr { }
}
Expect(9);
- Expect(24);
- Expect(8);
- VarOrType(out tyd);
- Expect(9);
+ if (t.kind == 24) {
+ Get();
+ Expect(8);
+ VarOrType(out tyd);
+ Expect(9);
+ retTyd = tyd;
+ } else if (t.kind == 10) {
+ Get();
+ Type(out retTy);
+ retTyd = new TypedIdent(retTy.tok, "", retTy);
+ } else Error(86);
if (t.kind == 25) {
Get();
Expression(out tmp);
@@ -294,42 +307,78 @@ private class BvBounds : Expr { Expect(26);
} else if (t.kind == 7) {
Get();
- } else Error(86);
+ } else Error(87);
+ if (retTyd == null) {
+ // construct a dummy type for the case of syntax error
+ tyd = new TypedIdent(token, "", new BasicType(token, SimpleType.Int));
+ } else {
+ tyd = retTyd;
+ }
Function! func = new Function(z, z.val, typeParams, arguments,
- new Formal(tyd.tok, tyd, false), null, kv);
+ new Formal(tyd.tok, tyd, false), null, kv);
ds.Add(func);
- if (definition != null) {
- // generate either an axiom or a function body
- if (QKeyValue.FindBoolAttribute(kv, "inline")) {
- func.Body = definition;
+ bool allUnnamed = true;
+ foreach (Formal! f in arguments) {
+ if (f.TypedIdent.Name != "") {
+ allUnnamed = false;
+ break;
+ }
+ }
+ if (!allUnnamed) {
+ Type prevType = null;
+ for (int i = arguments.Length - 1; i >= 0; i--) {
+ TypedIdent! curr = ((!)arguments[i]).TypedIdent;
+ if (curr.Name == "") {
+ if (prevType == null) {
+ SemErr(curr.tok, "the type of the last parameter is unspecified");
+ break;
+ }
+ Type ty = curr.Type;
+ if (ty is UnresolvedTypeIdentifier &&
+ ((!)(ty as UnresolvedTypeIdentifier)).Arguments.Length == 0) {
+ curr.Name = ((!)(ty as UnresolvedTypeIdentifier)).Name;
+ curr.Type = prevType;
} else {
- VariableSeq dummies = new VariableSeq();
- ExprSeq callArgs = new ExprSeq();
- int i = 0;
- foreach (Formal! f in arguments) {
- string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;
- dummies.Add(new BoundVariable(f.tok, new TypedIdent(f.tok, nm, f.TypedIdent.Type)));
- callArgs.Add(new IdentifierExpr(f.tok, nm));
- i++;
- }
- TypeVariableSeq! quantifiedTypeVars = new TypeVariableSeq ();
- foreach (TypeVariable! t in typeParams)
- quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name));
- Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs);
- // specify the type of the function, because it might be that
- // type parameters only occur in the output type
- call = Expr.CoerceType(z, call, (Type)tyd.Type.Clone());
- Expr def = Expr.Eq(call, definition);
- if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {
- def = new ForallExpr(z, quantifiedTypeVars, dummies,
- kv,
- new Trigger(z, true, new ExprSeq(call), null),
- def);
- }
- ds.Add(new Axiom(z, def, "autogenerated definition axiom", null));
+ SemErr(curr.tok, "expecting an identifier as parameter name");
}
- }
+ } else {
+ prevType = curr.Type;
+ }
+ }
+ }
+ if (definition != null) {
+ // generate either an axiom or a function body
+ if (QKeyValue.FindBoolAttribute(kv, "inline")) {
+ func.Body = definition;
+ } else {
+ VariableSeq dummies = new VariableSeq();
+ ExprSeq callArgs = new ExprSeq();
+ int i = 0;
+ foreach (Formal! f in arguments) {
+ string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;
+ dummies.Add(new BoundVariable(f.tok, new TypedIdent(f.tok, nm, f.TypedIdent.Type)));
+ callArgs.Add(new IdentifierExpr(f.tok, nm));
+ i++;
+ }
+ TypeVariableSeq! quantifiedTypeVars = new TypeVariableSeq ();
+ foreach (TypeVariable! t in typeParams)
+ quantifiedTypeVars.Add(new TypeVariable (Token.NoToken, t.Name));
+ Expr call = new NAryExpr(z, new FunctionCall(new IdentifierExpr(z, z.val)), callArgs);
+ // specify the type of the function, because it might be that
+ // type parameters only occur in the output type
+ call = Expr.CoerceType(z, call, (Type)tyd.Type.Clone());
+ Expr def = Expr.Eq(call, definition);
+ if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {
+ def = new ForallExpr(z, quantifiedTypeVars, dummies,
+ kv,
+ new Trigger(z, true, new ExprSeq(call), null),
+ def);
+ }
+ ds.Add(new Axiom(z, def, "autogenerated definition axiom", null));
+ }
+ }
+
}
static void Axiom(out Axiom! m) {
@@ -402,7 +451,7 @@ private class BvBounds : Expr { impl = new Implementation(x, x.val, typeParams,
Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null);
- } else Error(87);
+ } else Error(88);
proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
}
@@ -506,7 +555,7 @@ private class BvBounds : Expr { ty = new UnresolvedTypeIdentifier (tok, tok.val, args);
} else if (t.kind == 15 || t.kind == 17) {
MapType(out ty);
- } else Error(88);
+ } else Error(89);
}
static void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq! tyds) {
@@ -553,7 +602,7 @@ private class BvBounds : Expr { Get();
Type(out ty);
Expect(9);
- } else Error(89);
+ } else Error(90);
}
static void Ident(out IToken! x) {
@@ -582,7 +631,7 @@ private class BvBounds : Expr { } else if (t.kind == 15 || t.kind == 17) {
MapType(out ty);
ts.Add(ty);
- } else Error(90);
+ } else Error(91);
}
static void MapType(out Bpl.Type! ty) {
@@ -754,7 +803,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { SpecPrePost(true, pre, post);
} else if (t.kind == 34 || t.kind == 35) {
SpecPrePost(false, pre, post);
- } else Error(91);
+ } else Error(92);
}
static void ImplBody(out VariableSeq! locals, out StmtList! stmtList) {
@@ -782,7 +831,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { SpecBody(out locals, out blocks);
Expect(7);
pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv));
- } else Error(92);
+ } else Error(93);
} else if (t.kind == 35) {
Get();
tok = token;
@@ -797,8 +846,8 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { SpecBody(out locals, out blocks);
Expect(7);
post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv));
- } else Error(93);
- } else Error(94);
+ } else Error(94);
+ } else Error(95);
}
static void SpecBody(out VariableSeq! locals, out BlockSeq! blocks) {
@@ -849,7 +898,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
Expression(out e);
b = new Block(x,x.val,cs,new ReturnExprCmd(token,e));
- } else Error(95);
+ } else Error(96);
Expect(7);
}
@@ -893,7 +942,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { CallCmd(out cn);
Expect(7);
c = cn;
- } else Error(96);
+ } else Error(97);
}
static void StmtList(out StmtList! stmtList) {
@@ -977,7 +1026,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 45) {
BreakCmd(out bcmd);
ec = bcmd;
- } else Error(97);
+ } else Error(98);
}
static void TransferCmd(out TransferCmd! tc) {
@@ -995,7 +1044,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 39) {
Get();
tc = new ReturnCmd(token);
- } else Error(98);
+ } else Error(99);
Expect(7);
}
@@ -1020,7 +1069,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
StmtList(out els);
elseOption = els;
- } else Error(99);
+ } else Error(100);
}
ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption);
}
@@ -1079,7 +1128,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (StartOf(5)) {
Expression(out ee);
e = ee;
- } else Error(100);
+ } else Error(101);
Expect(9);
}
@@ -1117,7 +1166,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
Expect(7);
c = new AssignCmd(x, lhss, rhss);
- } else Error(101);
+ } else Error(102);
}
static void CallCmd(out Cmd! c) {
@@ -1180,7 +1229,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
Expect(9);
c = new CallCmd(x, first.val, es, ids);
- } else Error(102);
+ } else Error(103);
} else if (t.kind == 51) {
Get();
Ident(out first);
@@ -1234,7 +1283,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
Expect(9);
c = new CallCmd(x, first.val, es, ids);
- } else Error(103);
+ } else Error(104);
}
static void MapAssignIndexes(IToken! assignedVariable, out AssignLhs! lhs) {
@@ -1274,7 +1323,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (StartOf(5)) {
Expression(out e);
exprOptional = e;
- } else Error(104);
+ } else Error(105);
}
static void CallOutIdent(out IToken id) {
@@ -1286,7 +1335,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 1) {
Ident(out p);
id = p;
- } else Error(105);
+ } else Error(106);
}
static void Expressions(out ExprSeq! es) {
@@ -1331,7 +1380,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 53) {
Get();
- } else Error(106);
+ } else Error(107);
}
static void LogicalExpression(out Expr! e0) {
@@ -1369,7 +1418,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 55) {
Get();
- } else Error(107);
+ } else Error(108);
}
static void ExpliesOp() {
@@ -1377,7 +1426,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 57) {
Get();
- } else Error(108);
+ } else Error(109);
}
static void RelationalExpression(out Expr! e0) {
@@ -1395,7 +1444,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 59) {
Get();
- } else Error(109);
+ } else Error(110);
}
static void OrOp() {
@@ -1403,7 +1452,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 61) {
Get();
- } else Error(110);
+ } else Error(111);
}
static void BvTerm(out Expr! e0) {
@@ -1470,7 +1519,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { x = token; op=BinaryOperator.Opcode.Ge;
break;
}
- default: Error(111); break;
+ default: Error(112); break;
}
}
@@ -1502,7 +1551,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 72) {
Get();
x = token; op=BinaryOperator.Opcode.Sub;
- } else Error(112);
+ } else Error(113);
}
static void UnaryExpression(out Expr! e) {
@@ -1521,7 +1570,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
} else if (StartOf(12)) {
CoercionExpression(out e);
- } else Error(113);
+ } else Error(114);
}
static void MulOp(out IToken! x, out BinaryOperator.Opcode op) {
@@ -1535,7 +1584,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else if (t.kind == 74) {
Get();
x = token; op=BinaryOperator.Opcode.Mod;
- } else Error(114);
+ } else Error(115);
}
static void NegOp() {
@@ -1543,7 +1592,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 76) {
Get();
- } else Error(115);
+ } else Error(116);
}
static void CoercionExpression(out Expr! e) {
@@ -1567,7 +1616,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
}
- } else Error(116);
+ } else Error(117);
}
}
@@ -1677,7 +1726,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { e = new NAryExpr(x, new FunctionCall(id), es);
} else if (t.kind == 9) {
e = new NAryExpr(x, new FunctionCall(id), new ExprSeq());
- } else Error(117);
+ } else Error(118);
Expect(9);
}
break;
@@ -1710,11 +1759,11 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Length + ds.Length > 0)
e = new ExistsExpr(x, typeParams, ds, kv, trig, e);
- } else Error(118);
+ } else Error(119);
Expect(9);
break;
}
- default: Error(119); break;
+ default: Error(120); break;
}
}
@@ -1739,7 +1788,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
} else if (t.kind == 80) {
Get();
- } else Error(120);
+ } else Error(121);
}
static void QuantifierBody(IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds,
@@ -1756,7 +1805,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { }
} else if (t.kind == 1) {
BoundVars(q, out ds);
- } else Error(121);
+ } else Error(122);
QSep();
while (t.kind == 25) {
AttributeOrTrigger(ref kv, ref trig);
@@ -1769,7 +1818,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { Get();
} else if (t.kind == 82) {
Get();
- } else Error(122);
+ } else Error(123);
}
static void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
@@ -1825,7 +1874,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { trig.AddLast(new Trigger(tok, true, es, null));
}
- } else Error(123);
+ } else Error(124);
Expect(26);
}
@@ -1839,7 +1888,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { } else if (StartOf(5)) {
Expression(out e);
o = e;
- } else Error(124);
+ } else Error(125);
}
static void QSep() {
@@ -1847,7 +1896,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { Get();
} else if (t.kind == 84) {
Get();
- } else Error(125);
+ } else Error(126);
}
@@ -1953,45 +2002,46 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { case 84: s = "\\u2022 expected"; break;
case 85: s = "??? expected"; break;
case 86: s = "invalid Function"; break;
- case 87: s = "invalid Procedure"; break;
- case 88: s = "invalid Type"; break;
- case 89: s = "invalid TypeAtom"; break;
- case 90: s = "invalid TypeArgs"; break;
- case 91: s = "invalid Spec"; break;
- case 92: s = "invalid SpecPrePost"; break;
+ case 87: s = "invalid Function"; break;
+ case 88: s = "invalid Procedure"; break;
+ case 89: s = "invalid Type"; break;
+ case 90: s = "invalid TypeAtom"; break;
+ case 91: s = "invalid TypeArgs"; break;
+ case 92: s = "invalid Spec"; break;
case 93: s = "invalid SpecPrePost"; break;
case 94: s = "invalid SpecPrePost"; break;
- case 95: s = "invalid SpecBlock"; break;
- case 96: s = "invalid LabelOrCmd"; break;
- case 97: s = "invalid StructuredCmd"; break;
- case 98: s = "invalid TransferCmd"; break;
- case 99: s = "invalid IfCmd"; break;
- case 100: s = "invalid Guard"; break;
- case 101: s = "invalid LabelOrAssign"; break;
- case 102: s = "invalid CallCmd"; break;
+ case 95: s = "invalid SpecPrePost"; break;
+ case 96: s = "invalid SpecBlock"; break;
+ case 97: s = "invalid LabelOrCmd"; break;
+ case 98: s = "invalid StructuredCmd"; break;
+ case 99: s = "invalid TransferCmd"; break;
+ case 100: s = "invalid IfCmd"; break;
+ case 101: s = "invalid Guard"; break;
+ case 102: s = "invalid LabelOrAssign"; break;
case 103: s = "invalid CallCmd"; break;
- case 104: s = "invalid CallForallArg"; break;
- case 105: s = "invalid CallOutIdent"; break;
- case 106: s = "invalid EquivOp"; break;
- case 107: s = "invalid ImpliesOp"; break;
- case 108: s = "invalid ExpliesOp"; break;
- case 109: s = "invalid AndOp"; break;
- case 110: s = "invalid OrOp"; break;
- case 111: s = "invalid RelOp"; break;
- case 112: s = "invalid AddOp"; break;
- case 113: s = "invalid UnaryExpression"; break;
- case 114: s = "invalid MulOp"; break;
- case 115: s = "invalid NegOp"; break;
- case 116: s = "invalid CoercionExpression"; break;
- case 117: s = "invalid AtomExpression"; break;
+ case 104: s = "invalid CallCmd"; break;
+ case 105: s = "invalid CallForallArg"; break;
+ case 106: s = "invalid CallOutIdent"; break;
+ case 107: s = "invalid EquivOp"; break;
+ case 108: s = "invalid ImpliesOp"; break;
+ case 109: s = "invalid ExpliesOp"; break;
+ case 110: s = "invalid AndOp"; break;
+ case 111: s = "invalid OrOp"; break;
+ case 112: s = "invalid RelOp"; break;
+ case 113: s = "invalid AddOp"; break;
+ case 114: s = "invalid UnaryExpression"; break;
+ case 115: s = "invalid MulOp"; break;
+ case 116: s = "invalid NegOp"; break;
+ case 117: s = "invalid CoercionExpression"; break;
case 118: s = "invalid AtomExpression"; break;
case 119: s = "invalid AtomExpression"; break;
- case 120: s = "invalid Forall"; break;
- case 121: s = "invalid QuantifierBody"; break;
- case 122: s = "invalid Exists"; break;
- case 123: s = "invalid AttributeOrTrigger"; break;
- case 124: s = "invalid AttributeParameter"; break;
- case 125: s = "invalid QSep"; break;
+ case 120: s = "invalid AtomExpression"; break;
+ case 121: s = "invalid Forall"; break;
+ case 122: s = "invalid QuantifierBody"; break;
+ case 123: s = "invalid Exists"; break;
+ case 124: s = "invalid AttributeOrTrigger"; break;
+ case 125: s = "invalid AttributeParameter"; break;
+ case 126: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc index eb0c8b04..745f8dc4 100644 --- a/Source/Core/Scanner.ssc +++ b/Source/Core/Scanner.ssc @@ -1,8 +1,8 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- using System;
using System.IO;
using System.Collections;
@@ -433,7 +433,7 @@ public class Scanner { }
}
-
+ static bool Comment0() {
int level = 1, line0 = line, lineStart0 = lineStart;
NextCh();
@@ -456,7 +456,7 @@ public class Scanner { }
return false;
}
-
+ static bool Comment1() {
int level = 1, line0 = line, lineStart0 = lineStart;
NextCh();
diff --git a/Source/Core/parser.frame b/Source/Core/parser.frame index 81c7e67c..c7818e57 100644 --- a/Source/Core/parser.frame +++ b/Source/Core/parser.frame @@ -26,6 +26,10 @@ public class Parser { errDist = 0;
}
+ public static void SemErr(IToken! tok, string! msg) {
+ Errors.SemErr(tok.filename, tok.line, tok.col, msg);
+ }
+
static void Get() {
for (;;) {
token = t;
@@ -96,4 +100,4 @@ public class Parser { } // end Parser
} // end namespace
-$$$
\ No newline at end of file +$$$
|