summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-03-01 22:05:19 -0800
committerGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-03-01 22:05:19 -0800
commitabdbd2a717efd1e6184bf1113ed2cce63da0d0ea (patch)
tree192a5dac7dfcf28cc8278964f4dff4cb2a4273c3
parentc5c2c9465a53e4b35a20ad5efe73882dc6a5af34 (diff)
added parallel calls
Diffstat
-rw-r--r--Source/Core/AbsyCmd.cs134
-rw-r--r--Source/Core/BoogiePL.atg40
-rw-r--r--Source/Core/LinearSets.cs15
-rw-r--r--Source/Core/OwickiGries.cs153
-rw-r--r--Source/Core/Parser.cs467
-rw-r--r--Source/Core/ResolutionContext.cs2
-rw-r--r--Source/Core/Scanner.cs105
-rw-r--r--Source/Core/StandardVisitor.cs13
-rw-r--r--Test/og/Answer12
-rw-r--r--Test/og/DeviceCacheSimplified.bpl8
-rw-r--r--Test/og/FlanaganQadeer.bpl5
-rw-r--r--Test/og/bar.bpl9
-rw-r--r--Test/og/foo.bpl11
-rw-r--r--Test/og/linear-set.bpl16
-rw-r--r--Test/og/linear-set2.bpl16
-rw-r--r--Test/og/one.bpl3
-rw-r--r--Test/og/parallel1.bpl29
-rw-r--r--Test/og/parallel2.bpl35
-rw-r--r--Test/og/runtest.bat4
-rw-r--r--Test/prover/Answer16
20 files changed, 670 insertions, 423 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index af06b391..e62a98cb 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -944,18 +944,23 @@ namespace Microsoft.Boogie {
}
public abstract void Emit(TokenTextWriter/*!*/ stream, int level);
public abstract void AddAssignedVariables(VariableSeq/*!*/ vars);
- public void CheckAssignments(TypecheckingContext tc) {
- Contract.Requires(tc != null);
- VariableSeq/*!*/ vars = new VariableSeq();
- this.AddAssignedVariables(vars);
- foreach (Variable/*!*/ v in vars) {
- Contract.Assert(v != null);
- if (!v.IsMutable) {
- tc.Error(this, "command assigns to an immutable variable: {0}", v.Name);
- } else if (!CommandLineOptions.Clo.DoModSetAnalysis && v is GlobalVariable && !tc.InFrame(v)) {
- tc.Error(this, "command assigns to a global variable that is not in the enclosing method's modifies clause: {0}", v.Name);
+ public void CheckAssignments(TypecheckingContext tc)
+ {
+ Contract.Requires(tc != null);
+ VariableSeq/*!*/ vars = new VariableSeq();
+ this.AddAssignedVariables(vars);
+ foreach (Variable/*!*/ v in vars)
+ {
+ Contract.Assert(v != null);
+ if (!v.IsMutable)
+ {
+ tc.Error(this, "command assigns to an immutable variable: {0}", v.Name);
+ }
+ else if (!CommandLineOptions.Clo.DoModSetAnalysis && v is GlobalVariable && !tc.InFrame(v))
+ {
+ tc.Error(this, "command assigns to a global variable that is not in the enclosing method's modifies clause: {0}", v.Name);
+ }
}
- }
}
// Methods to simulate the old SimpleAssignCmd and MapAssignCmd
@@ -1060,6 +1065,37 @@ namespace Microsoft.Boogie {
}
}
+ public class YieldCmd : Cmd
+ {
+ public YieldCmd(IToken/*!*/ tok)
+ : base(tok)
+ {
+ Contract.Requires(tok != null);
+ }
+ public override void Emit(TokenTextWriter stream, int level)
+ {
+ //Contract.Requires(stream != null);
+ stream.Write(this, level, "yield;");
+ }
+ public override void Resolve(ResolutionContext rc)
+ {
+ // nothing to resolve
+ }
+ public override void Typecheck(TypecheckingContext tc)
+ {
+ // nothing to typecheck
+ }
+ public override void AddAssignedVariables(VariableSeq vars)
+ {
+ // nothing to add
+ }
+ public override Absy StdDispatch(StandardVisitor visitor)
+ {
+ Contract.Ensures(Contract.Result<Absy>() != null);
+ return visitor.VisitYieldCmd(this);
+ }
+ }
+
public class CommentCmd : Cmd // just a convenience for debugging
{
public readonly string/*!*/ Comment;
@@ -1688,6 +1724,7 @@ namespace Microsoft.Boogie {
}
public class CallCmd : CallCommonality, IPotentialErrorNode {
+ public CallCmd InParallelWith { get; private set; }
public string/*!*/ callee { get; private set; }
public Procedure Proc;
@@ -1761,6 +1798,18 @@ namespace Microsoft.Boogie {
this.Outs = outs;
}
+ public CallCmd(IToken tok, string callee, List<Expr> ins, List<IdentifierExpr> outs, QKeyValue kv, CallCmd inParallelWith)
+ : base(tok, kv)
+ {
+ Contract.Requires(outs != null);
+ Contract.Requires(ins != null);
+ Contract.Requires(callee != null);
+ Contract.Requires(tok != null);
+ this.callee = callee;
+ this.Ins = ins;
+ this.Outs = outs;
+ this.InParallelWith = inParallelWith;
+ }
public override void Emit(TokenTextWriter stream, int level) {
//Contract.Requires(stream != null);
stream.Write(this, level, "");
@@ -1818,14 +1867,23 @@ namespace Microsoft.Boogie {
if (ide != null) {
ide.Resolve(rc);
if (ide.Decl != null) {
- if (actualOuts[ide.Decl]) {
+ if (/* actualOuts[ide.Decl] */ rc.parallelCallLhss.Contains(ide.Decl)) {
rc.Error(this, "left-hand side of call command contains variable twice: {0}", ide.Name);
} else {
actualOuts.Add(ide.Decl);
+ rc.parallelCallLhss.Add(ide.Decl);
}
}
}
}
+ if (InParallelWith != null)
+ {
+ InParallelWith.Resolve(rc);
+ }
+ foreach (Variable v in actualOuts)
+ {
+ rc.parallelCallLhss.Remove(v);
+ }
if (Proc == null)
return;
@@ -1846,11 +1904,16 @@ namespace Microsoft.Boogie {
callee, Outs.Count);
return;
}
- if (QKeyValue.FindBoolAttribute(this.Attributes, "async")) {
+ if (IsAsync) {
if (Proc.OutParams.Length > 0) {
rc.Error(this.tok, "a procedure called asynchronously can have no output parameters");
return;
}
+ if (InParallelWith != null)
+ {
+ rc.Error(this.tok, "an asynchronous procedure call cannot be parallel");
+ return;
+ }
}
// Check that type parameters can be determined using the given
@@ -1941,6 +2004,10 @@ namespace Microsoft.Boogie {
Contract.Assert(cce.NonNullElements(actualTypeParams));
TypeParameters = SimpleTypeParamInstantiation.From(Proc.TypeParameters,
actualTypeParams);
+ if (InParallelWith != null)
+ {
+ InParallelWith.Typecheck(tc);
+ }
}
private IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ TypeParamSubstitution() {
@@ -2475,47 +2542,6 @@ namespace Microsoft.Boogie {
}
}
- public class YieldCmd : PredicateCmd
- {
- public YieldCmd(IToken/*!*/ tok, Expr/*!*/ expr)
- : base(tok, expr)
- {
- Contract.Requires(tok != null);
- Contract.Requires(expr != null);
- }
- public YieldCmd(IToken/*!*/ tok, Expr/*!*/ expr, QKeyValue kv)
- : base(tok, expr, kv)
- {
- Contract.Requires(tok != null);
- Contract.Requires(expr != null);
- }
- public override void Emit(TokenTextWriter stream, int level)
- {
- //Contract.Requires(stream != null);
- stream.Write(this, level, "assume ");
- EmitAttributes(stream, Attributes);
- this.Expr.Emit(stream);
- stream.WriteLine(";");
- }
- public override void Typecheck(TypecheckingContext tc)
- {
- //Contract.Requires(tc != null);
- Expr.Typecheck(tc);
- Contract.Assert(Expr.Type != null); // follows from Expr.Typecheck postcondition
- if (!Expr.Type.Unify(Type.Bool))
- {
- tc.Error(this, "an assumed expression must be of type bool (got: {0})", Expr.Type);
- }
- }
-
- public override Absy StdDispatch(StandardVisitor visitor)
- {
- //Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- return visitor.VisitYieldCmd(this);
- }
- }
-
public class ReturnExprCmd : ReturnCmd {
public Expr/*!*/ Expr;
[ContractInvariantMethod]
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 67c7fd9a..64ddbb50 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -855,10 +855,6 @@ LabelOrCmd<out Cmd c, out IToken label>
{ Attribute<ref kv> }
Proposition<out e> (. c = new AssumeCmd(x, e, kv); .)
";"
- | "yield" (. x = t; .)
- { Attribute<ref kv> }
- Proposition<out e> (. c = new YieldCmd(x, e, kv); .)
- ";"
| "havoc" (. x = t; .)
Idents<out xs> ";" (. ids = new IdentifierExprSeq();
foreach(IToken/*!*/ y in xs){
@@ -868,6 +864,8 @@ LabelOrCmd<out Cmd c, out IToken label>
c = new HavocCmd(x,ids);
.)
| CallCmd<out cn> ";" (. c = cn; .)
+ | "yield" (. x = t; .)
+ ";" (. c = new YieldCmd(x); .)
)
.
@@ -923,15 +921,13 @@ MapAssignIndex<.out IToken/*!*/ x, out List<Expr/*!*/>/*!*/ indexes.>
.
/*------------------------------------------------------------------------*/
-CallCmd<out Cmd/*!*/ c>
-= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x; IToken/*!*/ first; IToken p;
- List<IdentifierExpr>/*!*/ ids = new List<IdentifierExpr>();
- List<Expr>/*!*/ es = new List<Expr>();
- QKeyValue kv = null;
- Expr en; List<Expr> args;
- c = dummyCmd;
- bool isFree = false;
+CallCmd<out Cmd c>
+= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null);
+ IToken x;
bool isAsync = false;
+ bool isFree = false;
+ QKeyValue kv = null;
+ c = null;
.)
[ "async" (. isAsync = true; .)
]
@@ -939,13 +935,26 @@ CallCmd<out Cmd/*!*/ c>
]
"call" (. x = t; .)
{ Attribute<ref kv> }
- ( Ident<out first>
+ CallParams<isAsync, isFree, kv, x, ref c> (. .)
+ { "|" CallParams<isAsync, isFree, kv, x, ref c> (. .)
+ }
+ .
+
+CallParams<bool isAsync, bool isFree, QKeyValue kv, IToken x, ref Cmd c>
+= (.
+ List<IdentifierExpr> ids = new List<IdentifierExpr>();
+ List<Expr> es = new List<Expr>();
+ Expr en;
+ IToken first;
+ IToken p;
+ .)
+ Ident<out first>
( "("
[ Expression<out en> (. es.Add(en); .)
{ "," Expression<out en> (. es.Add(en); .)
}
]
- ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .)
+ ")" (. c = new CallCmd(x, first.val, es, ids, kv, (CallCmd) c); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .)
|
(. ids.Add(new IdentifierExpr(first, first.val)); .)
[ "," Ident<out p> (. ids.Add(new IdentifierExpr(p, p.val)); .)
@@ -957,9 +966,8 @@ CallCmd<out Cmd/*!*/ c>
{ "," Expression<out en> (. es.Add(en); .)
}
]
- ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .)
+ ")" (. c = new CallCmd(x, first.val, es, ids, kv, (CallCmd) c); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .)
)
- )
.
/*------------------------------------------------------------------------*/
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index de90b9e1..f409d67a 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -17,6 +17,7 @@ namespace Microsoft.Boogie
this.errorCount = 0;
this.checkingContext = new CheckingContext(null);
this.domainNameToType = new Dictionary<string, Type>();
+ this.parallelCallInvars = new HashSet<Variable>();
}
private void Error(Absy node, string message)
{
@@ -118,7 +119,7 @@ namespace Microsoft.Boogie
}
return base.VisitAssignCmd(node);
}
-
+ HashSet<Variable> parallelCallInvars;
public override Cmd VisitCallCmd(CallCmd node)
{
HashSet<Variable> inVars = new HashSet<Variable>();
@@ -144,7 +145,7 @@ namespace Microsoft.Boogie
Error(node, "The domains of formal and actual parameters must be the same");
continue;
}
- if (inVars.Contains(actual.Decl))
+ if (parallelCallInvars.Contains(actual.Decl))
{
Error(node, "A linear set can occur only once as an in parameter");
continue;
@@ -155,8 +156,8 @@ namespace Microsoft.Boogie
continue;
}
inVars.Add(actual.Decl);
+ parallelCallInvars.Add(actual.Decl);
}
-
for (int i = 0; i < node.Proc.OutParams.Length; i++)
{
IdentifierExpr actual = node.Outs[i];
@@ -180,6 +181,14 @@ namespace Microsoft.Boogie
continue;
}
}
+ if (node.InParallelWith != null)
+ {
+ VisitCallCmd(node.InParallelWith);
+ }
+ foreach (Variable v in inVars)
+ {
+ parallelCallInvars.Remove(v);
+ }
return base.VisitCallCmd(node);
}
}
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index 83509361..301f2a39 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -6,6 +6,7 @@ using System.Text;
using System.Threading.Tasks;
using Microsoft.Boogie;
using System.Diagnostics;
+using System.Diagnostics.Contracts;
namespace Microsoft.Boogie
{
@@ -19,6 +20,8 @@ namespace Microsoft.Boogie
public bool isEntrypoint;
// isAtomic is true if there are no yields transitively in any implementation
public bool isAtomic;
+ // inParallelCall is true iff this procedure is involved in some parallel call
+ public bool inParallelCall;
public Procedure yieldCheckerProc;
public Implementation yieldCheckerImpl;
public Procedure dummyAsyncTargetProc;
@@ -27,6 +30,7 @@ namespace Microsoft.Boogie
containsYield = false;
isThreadStart = false;
isAtomic = true;
+ inParallelCall = false;
yieldCheckerProc = null;
yieldCheckerImpl = null;
dummyAsyncTargetProc = null;
@@ -72,15 +76,12 @@ namespace Microsoft.Boogie
}
return base.VisitImplementation(node);
}
- public override Cmd VisitAssertCmd(AssertCmd node)
+ public override YieldCmd VisitYieldCmd(YieldCmd node)
{
- if (QKeyValue.FindBoolAttribute(node.Attributes, "yield"))
- {
- procNameToInfo[currentImpl.Name].containsYield = true;
- procNameToInfo[currentImpl.Name].isAtomic = false;
- CreateYieldCheckerProcedure(currentImpl.Proc);
- }
- return base.VisitAssertCmd(node);
+ procNameToInfo[currentImpl.Name].containsYield = true;
+ procNameToInfo[currentImpl.Name].isAtomic = false;
+ CreateYieldCheckerProcedure(currentImpl.Proc);
+ return base.VisitYieldCmd(node);
}
public override Cmd VisitCallCmd(CallCmd node)
{
@@ -88,7 +89,7 @@ namespace Microsoft.Boogie
{
procNameToInfo[node.Proc.Name] = new ProcedureInfo();
}
- if (QKeyValue.FindBoolAttribute(node.Attributes, "async"))
+ if (node.IsAsync)
{
procNameToInfo[node.Proc.Name].isThreadStart = true;
CreateYieldCheckerProcedure(node.Proc);
@@ -99,6 +100,15 @@ namespace Microsoft.Boogie
procNameToInfo[node.Proc.Name].dummyAsyncTargetProc = dummyAsyncTargetProc;
}
}
+ if (node.InParallelWith != null)
+ {
+ CallCmd iter = node;
+ while (iter != null)
+ {
+ procNameToInfo[iter.Proc.Name].inParallelCall = true;
+ iter = iter.InParallelWith;
+ }
+ }
return base.VisitCallCmd(node);
}
private void CreateYieldCheckerProcedure(Procedure proc)
@@ -138,7 +148,7 @@ namespace Microsoft.Boogie
public override Cmd VisitCallCmd(CallCmd node)
{
ProcedureInfo info = procNameToInfo[node.callee];
- if (!QKeyValue.FindBoolAttribute(node.Attributes, "async") && !info.isAtomic)
+ if (!node.IsAsync && !info.isAtomic)
{
procNameToInfo[currentImpl.Name].isAtomic = false;
moreProcessingRequired = true;
@@ -153,6 +163,7 @@ namespace Microsoft.Boogie
IdentifierExprSeq globalMods;
Hashtable ogOldGlobalMap;
Program program;
+ Dictionary<string, Procedure> parallelCallDesugarings;
public OwickiGriesTransform(Program program)
{
@@ -167,6 +178,7 @@ namespace Microsoft.Boogie
ogOldGlobalMap[g] = new IdentifierExpr(Token.NoToken, oldg);
globalMods.Add(new IdentifierExpr(Token.NoToken, g));
}
+ parallelCallDesugarings = new Dictionary<string, Procedure>();
}
private void AddCallsToYieldCheckers(CmdSeq newCmds)
@@ -209,6 +221,72 @@ namespace Microsoft.Boogie
}
}
+ public Procedure DesugarParallelCallCmd(CallCmd callCmd, out List<Expr> ins, out List<IdentifierExpr> outs)
+ {
+ List<string> parallelCalleeNames = new List<string>();
+ CallCmd iter = callCmd;
+ ins = new List<Expr>();
+ outs = new List<IdentifierExpr>();
+ while (iter != null)
+ {
+ parallelCalleeNames.Add(iter.Proc.Name);
+ ins.AddRange(iter.Ins);
+ outs.AddRange(iter.Outs);
+ iter = iter.InParallelWith;
+ }
+ parallelCalleeNames.Sort();
+ string procName = "og";
+ foreach (string calleeName in parallelCalleeNames)
+ {
+ procName = procName + "@" + calleeName;
+ }
+ if (parallelCallDesugarings.ContainsKey(procName))
+ return parallelCallDesugarings[procName];
+
+ VariableSeq inParams = new VariableSeq();
+ VariableSeq outParams = new VariableSeq();
+ RequiresSeq requiresSeq = new RequiresSeq();
+ EnsuresSeq ensuresSeq = new EnsuresSeq();
+ IdentifierExprSeq ieSeq = new IdentifierExprSeq();
+ int count = 0;
+ while (callCmd != null)
+ {
+ Hashtable map = new Hashtable();
+ foreach (Variable x in callCmd.Proc.InParams)
+ {
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og@" + count + x.Name, x.TypedIdent.Type), true);
+ inParams.Add(y);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ }
+ foreach (Variable x in callCmd.Proc.OutParams)
+ {
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og@" + count + x.Name, x.TypedIdent.Type), false);
+ outParams.Add(y);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ }
+ Contract.Assume(callCmd.Proc.TypeParameters.Length == 0);
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ foreach (Requires req in callCmd.Proc.Requires)
+ {
+ requiresSeq.Add(new Requires(req.Free, Substituter.Apply(subst, req.Condition)));
+ }
+ foreach (IdentifierExpr ie in callCmd.Proc.Modifies)
+ {
+ ieSeq.Add(ie);
+ }
+ foreach (Ensures ens in callCmd.Proc.Ensures)
+ {
+ ensuresSeq.Add(new Ensures(ens.Free, Substituter.Apply(subst, ens.Condition)));
+ }
+ count++;
+ callCmd = callCmd.InParallelWith;
+ }
+
+ Procedure proc = new Procedure(Token.NoToken, procName, new TypeVariableSeq(), inParams, outParams, requiresSeq, ieSeq, ensuresSeq);
+ parallelCallDesugarings[procName] = proc;
+ return proc;
+ }
+
public void Transform()
{
foreach (var decl in program.TopLevelDeclarations)
@@ -278,32 +356,59 @@ namespace Microsoft.Boogie
yields.Add(cmds);
cmds = new CmdSeq();
}
+ if (info.inParallelCall && impl.Proc.Ensures.Length > 0)
+ {
+ foreach (Ensures e in impl.Proc.Ensures)
+ {
+ if (e.Free) continue;
+ cmds.Add(new AssertCmd(Token.NoToken, e.Condition));
+ }
+ yields.Add(cmds);
+ cmds = new CmdSeq();
+ }
foreach (Block b in impl.Blocks)
{
bool insideYield = false;
CmdSeq newCmds = new CmdSeq();
for (int i = 0; i < b.Cmds.Length; i++)
{
- PredicateCmd pcmd = b.Cmds[i] as PredicateCmd;
- if (pcmd == null || QKeyValue.FindBoolAttribute(pcmd.Attributes, "yield"))
+ Cmd cmd = b.Cmds[i];
+ if (cmd is YieldCmd)
{
- if (cmds.Length > 0)
- {
- DesugarYield(cmds, newCmds);
- yields.Add(cmds);
- cmds = new CmdSeq();
- }
- insideYield = (pcmd != null);
+ insideYield = true;
+ continue;
}
if (insideYield)
{
- cmds.Add(pcmd);
+ PredicateCmd pcmd = cmd as PredicateCmd;
+ if (pcmd == null)
+ {
+ if (cmds.Length > 0)
+ {
+ DesugarYield(cmds, newCmds);
+ yields.Add(cmds);
+ cmds = new CmdSeq();
+ }
+ insideYield = false;
+ }
+ else
+ {
+ cmds.Add(pcmd);
+ }
}
-
- CallCmd callCmd = b.Cmds[i] as CallCmd;
+ CallCmd callCmd = cmd as CallCmd;
if (callCmd != null)
{
- if (QKeyValue.FindBoolAttribute(callCmd.Attributes, "async"))
+ if (callCmd.InParallelWith != null)
+ {
+ List<Expr> ins;
+ List<IdentifierExpr> outs;
+ Procedure dummyParallelCallDesugaring = DesugarParallelCallCmd(callCmd, out ins, out outs);
+ CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyParallelCallDesugaring.Name, ins, outs);
+ dummyCallCmd.Proc = dummyParallelCallDesugaring;
+ newCmds.Add(dummyCallCmd);
+ }
+ else if (callCmd.IsAsync)
{
var dummyAsyncTargetProc = procNameToInfo[callCmd.callee].dummyAsyncTargetProc;
CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);
@@ -323,7 +428,7 @@ namespace Microsoft.Boogie
}
else
{
- newCmds.Add(b.Cmds[i]);
+ newCmds.Add(cmd);
}
}
if (cmds.Length > 0)
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index a6af2c45..95c46934 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -25,7 +25,7 @@ public class Parser {
public const int _string = 4;
public const int _decimal = 5;
public const int _float = 6;
- public const int maxT = 94;
+ public const int maxT = 95;
const bool T = true;
const bool x = false;
@@ -363,7 +363,7 @@ private class BvBounds : Expr {
Get();
Type(out retTy);
retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy);
- } else SynErr(95);
+ } else SynErr(96);
if (la.kind == 27) {
Get();
Expression(out tmp);
@@ -371,7 +371,7 @@ private class BvBounds : Expr {
Expect(28);
} else if (la.kind == 8) {
Get();
- } else SynErr(96);
+ } else SynErr(97);
if (retTyd == null) {
// construct a dummy type for the case of syntax error
retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int));
@@ -494,7 +494,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(97);
+ } else SynErr(98);
proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
}
@@ -606,7 +606,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(98);
+ } else SynErr(99);
}
void AttributesIdsTypeWhere(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
@@ -647,7 +647,7 @@ private class BvBounds : Expr {
void Expression(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
ImpliesExpression(false, out e0);
- while (la.kind == 53 || la.kind == 54) {
+ while (la.kind == 54 || la.kind == 55) {
EquivOp();
x = t;
ImpliesExpression(false, out e1);
@@ -670,7 +670,7 @@ private class BvBounds : Expr {
Get();
Type(out ty);
Expect(10);
- } else SynErr(99);
+ } else SynErr(100);
}
void Ident(out IToken/*!*/ x) {
@@ -700,7 +700,7 @@ private class BvBounds : Expr {
} else if (la.kind == 17 || la.kind == 19) {
MapType(out ty);
ts.Add(ty);
- } else SynErr(100);
+ } else SynErr(101);
}
void MapType(out Bpl.Type/*!*/ ty) {
@@ -885,7 +885,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
SpecPrePost(true, pre, post);
} else if (la.kind == 36 || la.kind == 37) {
SpecPrePost(false, pre, post);
- } else SynErr(101);
+ } else SynErr(102);
}
void ImplBody(out VariableSeq/*!*/ locals, out StmtList/*!*/ stmtList) {
@@ -917,7 +917,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
Proposition(out e);
Expect(8);
post.Add(new Ensures(tok, free, e, null, kv));
- } else SynErr(102);
+ } else SynErr(103);
}
void StmtList(out StmtList/*!*/ stmtList) {
@@ -1027,17 +1027,6 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
case 48: {
Get();
x = t;
- while (la.kind == 27) {
- Attribute(ref kv);
- }
- Proposition(out e);
- c = new YieldCmd(x, e, kv);
- Expect(8);
- break;
- }
- case 49: {
- Get();
- x = t;
Idents(out xs);
Expect(8);
ids = new IdentifierExprSeq();
@@ -1055,7 +1044,14 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
c = cn;
break;
}
- default: SynErr(103); break;
+ case 49: {
+ Get();
+ x = t;
+ Expect(8);
+ c = new YieldCmd(x);
+ break;
+ }
+ default: SynErr(104); break;
}
}
@@ -1072,7 +1068,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
} else if (la.kind == 45) {
BreakCmd(out bcmd);
ec = bcmd;
- } else SynErr(104);
+ } else SynErr(105);
}
void TransferCmd(out TransferCmd/*!*/ tc) {
@@ -1092,7 +1088,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
} else if (la.kind == 39) {
Get();
tc = new ReturnCmd(t);
- } else SynErr(105);
+ } else SynErr(106);
Expect(8);
}
@@ -1117,7 +1113,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
Get();
StmtList(out els);
elseOption = els;
- } else SynErr(106);
+ } else SynErr(107);
}
ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption);
}
@@ -1180,7 +1176,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
} else if (StartOf(9)) {
Expression(out ee);
e = ee;
- } else SynErr(107);
+ } else SynErr(108);
Expect(10);
}
@@ -1227,18 +1223,16 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
Expect(8);
c = new AssignCmd(x, lhss, rhss);
- } else SynErr(108);
+ } else SynErr(109);
}
- void CallCmd(out Cmd/*!*/ c) {
- Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x; IToken/*!*/ first; IToken p;
- List<IdentifierExpr>/*!*/ ids = new List<IdentifierExpr>();
- List<Expr>/*!*/ es = new List<Expr>();
- QKeyValue kv = null;
- Expr en; List<Expr> args;
- c = dummyCmd;
- bool isFree = false;
+ void CallCmd(out Cmd c) {
+ Contract.Ensures(Contract.ValueAtReturn(out c) != null);
+ IToken x;
bool isAsync = false;
+ bool isFree = false;
+ QKeyValue kv = null;
+ c = null;
if (la.kind == 51) {
Get();
@@ -1253,6 +1247,40 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
while (la.kind == 27) {
Attribute(ref kv);
}
+ CallParams(isAsync, isFree, kv, x, ref c);
+
+ while (la.kind == 53) {
+ Get();
+ CallParams(isAsync, isFree, kv, x, ref c);
+
+ }
+ }
+
+ void MapAssignIndex(out IToken/*!*/ x, out List<Expr/*!*/>/*!*/ indexes) {
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List<Expr/*!*/> ();
+ Expr/*!*/ e;
+
+ Expect(17);
+ x = t;
+ if (StartOf(9)) {
+ Expression(out e);
+ indexes.Add(e);
+ while (la.kind == 12) {
+ Get();
+ Expression(out e);
+ indexes.Add(e);
+ }
+ }
+ Expect(18);
+ }
+
+ void CallParams(bool isAsync, bool isFree, QKeyValue kv, IToken x, ref Cmd c) {
+ List<IdentifierExpr> ids = new List<IdentifierExpr>();
+ List<Expr> es = new List<Expr>();
+ Expr en;
+ IToken first;
+ IToken p;
+
Ident(out first);
if (la.kind == 9) {
Get();
@@ -1266,7 +1294,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
}
Expect(10);
- c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync;
+ c = new CallCmd(x, first.val, es, ids, kv, (CallCmd) c); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync;
} else if (la.kind == 12 || la.kind == 50) {
ids.Add(new IdentifierExpr(first, first.val));
if (la.kind == 12) {
@@ -1292,26 +1320,8 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ 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(109);
- }
-
- void MapAssignIndex(out IToken/*!*/ x, out List<Expr/*!*/>/*!*/ indexes) {
- Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List<Expr/*!*/> ();
- Expr/*!*/ e;
-
- Expect(17);
- x = t;
- if (StartOf(9)) {
- Expression(out e);
- indexes.Add(e);
- while (la.kind == 12) {
- Get();
- Expression(out e);
- indexes.Add(e);
- }
- }
- Expect(18);
+ c = new CallCmd(x, first.val, es, ids, kv, (CallCmd) c); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync;
+ } else SynErr(110);
}
void Expressions(out ExprSeq/*!*/ es) {
@@ -1329,7 +1339,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
LogicalExpression(out e0);
if (StartOf(10)) {
- if (la.kind == 55 || la.kind == 56) {
+ if (la.kind == 56 || la.kind == 57) {
ImpliesOp();
x = t;
ImpliesExpression(true, out e1);
@@ -1341,7 +1351,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
x = t;
LogicalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
- while (la.kind == 57 || la.kind == 58) {
+ while (la.kind == 58 || la.kind == 59) {
ExpliesOp();
x = t;
LogicalExpression(out e1);
@@ -1352,23 +1362,23 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
void EquivOp() {
- if (la.kind == 53) {
+ if (la.kind == 54) {
Get();
- } else if (la.kind == 54) {
+ } else if (la.kind == 55) {
Get();
- } else SynErr(110);
+ } else SynErr(111);
}
void LogicalExpression(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(11)) {
- if (la.kind == 59 || la.kind == 60) {
+ if (la.kind == 60 || la.kind == 61) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
- while (la.kind == 59 || la.kind == 60) {
+ while (la.kind == 60 || la.kind == 61) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1379,7 +1389,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
x = t;
RelationalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
- while (la.kind == 61 || la.kind == 62) {
+ while (la.kind == 62 || la.kind == 63) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1390,19 +1400,19 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
void ImpliesOp() {
- if (la.kind == 55) {
+ if (la.kind == 56) {
Get();
- } else if (la.kind == 56) {
+ } else if (la.kind == 57) {
Get();
- } else SynErr(111);
+ } else SynErr(112);
}
void ExpliesOp() {
- if (la.kind == 57) {
+ if (la.kind == 58) {
Get();
- } else if (la.kind == 58) {
+ } else if (la.kind == 59) {
Get();
- } else SynErr(112);
+ } else SynErr(113);
}
void RelationalExpression(out Expr/*!*/ e0) {
@@ -1416,25 +1426,25 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
void AndOp() {
- if (la.kind == 59) {
+ if (la.kind == 60) {
Get();
- } else if (la.kind == 60) {
+ } else if (la.kind == 61) {
Get();
- } else SynErr(113);
+ } else SynErr(114);
}
void OrOp() {
- if (la.kind == 61) {
+ if (la.kind == 62) {
Get();
- } else if (la.kind == 62) {
+ } else if (la.kind == 63) {
Get();
- } else SynErr(114);
+ } else SynErr(115);
}
void BvTerm(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
Term(out e0);
- while (la.kind == 71) {
+ while (la.kind == 72) {
Get();
x = t;
Term(out e1);
@@ -1445,7 +1455,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
switch (la.kind) {
- case 63: {
+ case 64: {
Get();
x = t; op=BinaryOperator.Opcode.Eq;
break;
@@ -1460,49 +1470,49 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
x = t; op=BinaryOperator.Opcode.Gt;
break;
}
- case 64: {
+ case 65: {
Get();
x = t; op=BinaryOperator.Opcode.Le;
break;
}
- case 65: {
+ case 66: {
Get();
x = t; op=BinaryOperator.Opcode.Ge;
break;
}
- case 66: {
+ case 67: {
Get();
x = t; op=BinaryOperator.Opcode.Neq;
break;
}
- case 67: {
+ case 68: {
Get();
x = t; op=BinaryOperator.Opcode.Subtype;
break;
}
- case 68: {
+ case 69: {
Get();
x = t; op=BinaryOperator.Opcode.Neq;
break;
}
- case 69: {
+ case 70: {
Get();
x = t; op=BinaryOperator.Opcode.Le;
break;
}
- case 70: {
+ case 71: {
Get();
x = t; op=BinaryOperator.Opcode.Ge;
break;
}
- default: SynErr(115); break;
+ default: SynErr(116); break;
}
}
void Term(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op;
Factor(out e0);
- while (la.kind == 72 || la.kind == 73) {
+ while (la.kind == 73 || la.kind == 74) {
AddOp(out x, out op);
Factor(out e1);
e0 = Expr.Binary(x, op, e0, e1);
@@ -1521,19 +1531,19 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
- if (la.kind == 72) {
+ if (la.kind == 73) {
Get();
x = t; op=BinaryOperator.Opcode.Add;
- } else if (la.kind == 73) {
+ } else if (la.kind == 74) {
Get();
x = t; op=BinaryOperator.Opcode.Sub;
- } else SynErr(116);
+ } else SynErr(117);
}
void Power(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
UnaryExpression(out e0);
- if (la.kind == 77) {
+ if (la.kind == 78) {
Get();
x = t;
Power(out e1);
@@ -1546,43 +1556,43 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
if (la.kind == 44) {
Get();
x = t; op=BinaryOperator.Opcode.Mul;
- } else if (la.kind == 74) {
+ } else if (la.kind == 75) {
Get();
x = t; op=BinaryOperator.Opcode.Div;
- } else if (la.kind == 75) {
+ } else if (la.kind == 76) {
Get();
x = t; op=BinaryOperator.Opcode.Mod;
- } else if (la.kind == 76) {
+ } else if (la.kind == 77) {
Get();
x = t; op=BinaryOperator.Opcode.RealDiv;
- } else SynErr(117);
+ } else SynErr(118);
}
void UnaryExpression(out Expr/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
e = dummyExpr;
- if (la.kind == 73) {
+ if (la.kind == 74) {
Get();
x = t;
UnaryExpression(out e);
e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e);
- } else if (la.kind == 78 || la.kind == 79) {
+ } else if (la.kind == 79 || la.kind == 80) {
NegOp();
x = t;
UnaryExpression(out e);
e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
} else if (StartOf(14)) {
CoercionExpression(out e);
- } else SynErr(118);
+ } else SynErr(119);
}
void NegOp() {
- if (la.kind == 78) {
+ if (la.kind == 79) {
Get();
- } else if (la.kind == 79) {
+ } else if (la.kind == 80) {
Get();
- } else SynErr(119);
+ } else SynErr(120);
}
void CoercionExpression(out Expr/*!*/ e) {
@@ -1606,7 +1616,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
}
- } else SynErr(120);
+ } else SynErr(121);
}
}
@@ -1687,12 +1697,12 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
List<Block/*!*/>/*!*/ blocks;
switch (la.kind) {
- case 80: {
+ case 81: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 81: {
+ case 82: {
Get();
e = new LiteralExpr(t, true);
break;
@@ -1722,12 +1732,12 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ 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 ExprSeq());
- } else SynErr(121);
+ } else SynErr(122);
Expect(10);
}
break;
}
- case 82: {
+ case 83: {
Get();
x = t;
Expect(9);
@@ -1761,19 +1771,19 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
if (e is BvBounds)
this.SemErr("parentheses around bitvector bounds " +
"are not allowed");
- } else if (la.kind == 86 || la.kind == 87) {
+ } else if (la.kind == 87 || la.kind == 88) {
Forall();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Length + ds.Length > 0)
e = new ForallExpr(x, typeParams, ds, kv, trig, e);
- } else if (la.kind == 88 || la.kind == 89) {
+ } else if (la.kind == 89 || la.kind == 90) {
Exists();
x = t;
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 if (la.kind == 90 || la.kind == 91) {
+ } else if (la.kind == 91 || la.kind == 92) {
Lambda();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
@@ -1781,7 +1791,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
SemErr("triggers not allowed in lambda expressions");
if (typeParams.Length + ds.Length > 0)
e = new LambdaExpr(x, typeParams, ds, kv, e);
- } else SynErr(122);
+ } else SynErr(123);
Expect(10);
break;
}
@@ -1789,12 +1799,12 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
IfThenElseExpression(out e);
break;
}
- case 83: {
+ case 84: {
CodeExpression(out locals, out blocks);
e = new CodeExpr(locals, blocks);
break;
}
- default: SynErr(123); break;
+ default: SynErr(124); break;
}
}
@@ -1806,7 +1816,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
} else if (la.kind == 6) {
Get();
s = t.val;
- } else SynErr(124);
+ } else SynErr(125);
try {
n = BigDec.FromString(s);
} catch (FormatException) {
@@ -1833,11 +1843,11 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
}
void Forall() {
- if (la.kind == 86) {
+ if (la.kind == 87) {
Get();
- } else if (la.kind == 87) {
+ } else if (la.kind == 88) {
Get();
- } else SynErr(125);
+ } else SynErr(126);
}
void QuantifierBody(IToken/*!*/ q, out TypeVariableSeq/*!*/ typeParams, out VariableSeq/*!*/ ds,
@@ -1855,7 +1865,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
}
} else if (la.kind == 1 || la.kind == 27) {
BoundVars(q, out ds);
- } else SynErr(126);
+ } else SynErr(127);
QSep();
while (la.kind == 27) {
AttributeOrTrigger(ref kv, ref trig);
@@ -1864,19 +1874,19 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
}
void Exists() {
- if (la.kind == 88) {
+ if (la.kind == 89) {
Get();
- } else if (la.kind == 89) {
+ } else if (la.kind == 90) {
Get();
- } else SynErr(127);
+ } else SynErr(128);
}
void Lambda() {
- if (la.kind == 90) {
+ if (la.kind == 91) {
Get();
- } else if (la.kind == 91) {
+ } else if (la.kind == 92) {
Get();
- } else SynErr(128);
+ } else SynErr(129);
}
void IfThenElseExpression(out Expr/*!*/ e) {
@@ -1887,7 +1897,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Expect(40);
tok = t;
Expression(out e0);
- Expect(85);
+ Expect(86);
Expression(out e1);
Expect(41);
Expression(out e2);
@@ -1898,7 +1908,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new VariableSeq(); Block/*!*/ b;
blocks = new List<Block/*!*/>();
- Expect(83);
+ Expect(84);
while (la.kind == 7) {
LocalVars(locals);
}
@@ -1908,7 +1918,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
SpecBlock(out b);
blocks.Add(b);
}
- Expect(84);
+ Expect(85);
}
void SpecBlock(out Block/*!*/ b) {
@@ -1946,7 +1956,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(129);
+ } else SynErr(130);
Expect(8);
}
@@ -2003,7 +2013,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
trig.AddLast(new Trigger(tok, true, es, null));
}
- } else SynErr(130);
+ } else SynErr(131);
Expect(28);
}
@@ -2018,15 +2028,15 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
} else if (StartOf(9)) {
Expression(out e);
o = e;
- } else SynErr(131);
+ } else SynErr(132);
}
void QSep() {
- if (la.kind == 92) {
+ if (la.kind == 93) {
Get();
- } else if (la.kind == 93) {
+ } else if (la.kind == 94) {
Get();
- } else SynErr(132);
+ } else SynErr(133);
}
@@ -2042,23 +2052,23 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
}
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,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,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,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,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,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,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,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,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,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,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,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, 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,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,T,x,x, x,x,T,T, T,T,T,T, 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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,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,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,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, 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, x,x,x,x, x,x,x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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, 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, 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, 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,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,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,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,T,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x}
};
} // end Parser
@@ -2131,91 +2141,92 @@ public class Errors {
case 45: s = "\"break\" expected"; break;
case 46: s = "\"assert\" expected"; break;
case 47: s = "\"assume\" expected"; break;
- case 48: s = "\"yield\" expected"; break;
- case 49: s = "\"havoc\" expected"; break;
+ case 48: s = "\"havoc\" expected"; break;
+ case 49: s = "\"yield\" expected"; break;
case 50: s = "\":=\" expected"; break;
case 51: s = "\"async\" expected"; break;
case 52: s = "\"call\" expected"; break;
- case 53: s = "\"<==>\" expected"; break;
- case 54: s = "\"\\u21d4\" expected"; break;
- case 55: s = "\"==>\" expected"; break;
- case 56: s = "\"\\u21d2\" expected"; break;
- case 57: s = "\"<==\" expected"; break;
- case 58: s = "\"\\u21d0\" expected"; break;
- case 59: s = "\"&&\" expected"; break;
- case 60: s = "\"\\u2227\" expected"; break;
- case 61: s = "\"||\" expected"; break;
- case 62: s = "\"\\u2228\" expected"; break;
- case 63: s = "\"==\" expected"; break;
- case 64: s = "\"<=\" expected"; break;
- case 65: s = "\">=\" expected"; break;
- case 66: s = "\"!=\" expected"; break;
- case 67: s = "\"<:\" expected"; break;
- case 68: s = "\"\\u2260\" expected"; break;
- case 69: s = "\"\\u2264\" expected"; break;
- case 70: s = "\"\\u2265\" expected"; break;
- case 71: s = "\"++\" expected"; break;
- case 72: s = "\"+\" expected"; break;
- case 73: s = "\"-\" expected"; break;
- case 74: s = "\"div\" expected"; break;
- case 75: s = "\"mod\" expected"; break;
- case 76: s = "\"/\" expected"; break;
- case 77: s = "\"**\" expected"; break;
- case 78: s = "\"!\" expected"; break;
- case 79: s = "\"\\u00ac\" expected"; break;
- case 80: s = "\"false\" expected"; break;
- case 81: s = "\"true\" expected"; break;
- case 82: s = "\"old\" expected"; break;
- case 83: s = "\"|{\" expected"; break;
- case 84: s = "\"}|\" expected"; break;
- case 85: s = "\"then\" expected"; break;
- case 86: s = "\"forall\" expected"; break;
- case 87: s = "\"\\u2200\" expected"; break;
- case 88: s = "\"exists\" expected"; break;
- case 89: s = "\"\\u2203\" expected"; break;
- case 90: s = "\"lambda\" expected"; break;
- case 91: s = "\"\\u03bb\" expected"; break;
- case 92: s = "\"::\" expected"; break;
- case 93: s = "\"\\u2022\" expected"; break;
- case 94: s = "??? expected"; break;
- case 95: s = "invalid Function"; break;
+ case 53: s = "\"|\" expected"; break;
+ case 54: s = "\"<==>\" expected"; break;
+ case 55: s = "\"\\u21d4\" expected"; break;
+ case 56: s = "\"==>\" expected"; break;
+ case 57: s = "\"\\u21d2\" expected"; break;
+ case 58: s = "\"<==\" expected"; break;
+ case 59: s = "\"\\u21d0\" expected"; break;
+ case 60: s = "\"&&\" expected"; break;
+ case 61: s = "\"\\u2227\" expected"; break;
+ case 62: s = "\"||\" expected"; break;
+ case 63: s = "\"\\u2228\" expected"; break;
+ case 64: s = "\"==\" expected"; break;
+ case 65: s = "\"<=\" expected"; break;
+ case 66: s = "\">=\" expected"; break;
+ case 67: s = "\"!=\" expected"; break;
+ case 68: s = "\"<:\" expected"; break;
+ case 69: s = "\"\\u2260\" expected"; break;
+ case 70: s = "\"\\u2264\" expected"; break;
+ case 71: s = "\"\\u2265\" expected"; break;
+ case 72: s = "\"++\" expected"; break;
+ case 73: s = "\"+\" expected"; break;
+ case 74: s = "\"-\" expected"; break;
+ case 75: s = "\"div\" expected"; break;
+ case 76: s = "\"mod\" expected"; break;
+ case 77: s = "\"/\" expected"; break;
+ case 78: s = "\"**\" expected"; break;
+ case 79: s = "\"!\" expected"; break;
+ case 80: s = "\"\\u00ac\" expected"; break;
+ case 81: s = "\"false\" expected"; break;
+ case 82: s = "\"true\" expected"; break;
+ case 83: s = "\"old\" expected"; break;
+ case 84: s = "\"|{\" expected"; break;
+ case 85: s = "\"}|\" expected"; break;
+ case 86: s = "\"then\" expected"; break;
+ case 87: s = "\"forall\" expected"; break;
+ case 88: s = "\"\\u2200\" expected"; break;
+ case 89: s = "\"exists\" expected"; break;
+ case 90: s = "\"\\u2203\" expected"; break;
+ case 91: s = "\"lambda\" expected"; break;
+ case 92: s = "\"\\u03bb\" expected"; break;
+ case 93: s = "\"::\" expected"; break;
+ case 94: s = "\"\\u2022\" expected"; break;
+ case 95: s = "??? expected"; break;
case 96: s = "invalid Function"; break;
- case 97: s = "invalid Procedure"; break;
- case 98: s = "invalid Type"; break;
- case 99: s = "invalid TypeAtom"; break;
- case 100: s = "invalid TypeArgs"; break;
- case 101: s = "invalid Spec"; break;
- case 102: s = "invalid SpecPrePost"; break;
- case 103: s = "invalid LabelOrCmd"; break;
- case 104: s = "invalid StructuredCmd"; break;
- case 105: s = "invalid TransferCmd"; break;
- case 106: s = "invalid IfCmd"; break;
- case 107: s = "invalid Guard"; break;
- case 108: s = "invalid LabelOrAssign"; break;
- case 109: s = "invalid CallCmd"; break;
- case 110: s = "invalid EquivOp"; break;
- case 111: s = "invalid ImpliesOp"; break;
- case 112: s = "invalid ExpliesOp"; break;
- case 113: s = "invalid AndOp"; break;
- case 114: s = "invalid OrOp"; break;
- case 115: s = "invalid RelOp"; break;
- case 116: s = "invalid AddOp"; break;
- case 117: s = "invalid MulOp"; break;
- case 118: s = "invalid UnaryExpression"; break;
- case 119: s = "invalid NegOp"; break;
- case 120: s = "invalid CoercionExpression"; break;
- case 121: s = "invalid AtomExpression"; break;
+ case 97: s = "invalid Function"; break;
+ case 98: s = "invalid Procedure"; break;
+ case 99: s = "invalid Type"; break;
+ case 100: s = "invalid TypeAtom"; break;
+ case 101: s = "invalid TypeArgs"; break;
+ case 102: s = "invalid Spec"; break;
+ case 103: s = "invalid SpecPrePost"; break;
+ case 104: s = "invalid LabelOrCmd"; break;
+ case 105: s = "invalid StructuredCmd"; break;
+ case 106: s = "invalid TransferCmd"; break;
+ case 107: s = "invalid IfCmd"; break;
+ case 108: s = "invalid Guard"; break;
+ case 109: s = "invalid LabelOrAssign"; break;
+ case 110: s = "invalid CallParams"; break;
+ case 111: s = "invalid EquivOp"; break;
+ case 112: s = "invalid ImpliesOp"; break;
+ case 113: s = "invalid ExpliesOp"; break;
+ case 114: s = "invalid AndOp"; break;
+ case 115: s = "invalid OrOp"; break;
+ case 116: s = "invalid RelOp"; break;
+ case 117: s = "invalid AddOp"; break;
+ case 118: s = "invalid MulOp"; break;
+ case 119: s = "invalid UnaryExpression"; break;
+ case 120: s = "invalid NegOp"; break;
+ case 121: s = "invalid CoercionExpression"; break;
case 122: s = "invalid AtomExpression"; break;
case 123: s = "invalid AtomExpression"; break;
- case 124: s = "invalid Dec"; break;
- case 125: s = "invalid Forall"; break;
- case 126: s = "invalid QuantifierBody"; break;
- case 127: s = "invalid Exists"; break;
- case 128: s = "invalid Lambda"; break;
- case 129: s = "invalid SpecBlock"; break;
- case 130: s = "invalid AttributeOrTrigger"; break;
- case 131: s = "invalid AttributeParameter"; break;
- case 132: s = "invalid QSep"; break;
+ case 124: s = "invalid AtomExpression"; break;
+ case 125: s = "invalid Dec"; break;
+ case 126: s = "invalid Forall"; break;
+ case 127: s = "invalid QuantifierBody"; break;
+ case 128: s = "invalid Exists"; break;
+ case 129: s = "invalid Lambda"; break;
+ case 130: s = "invalid SpecBlock"; break;
+ case 131: s = "invalid AttributeOrTrigger"; break;
+ case 132: s = "invalid AttributeParameter"; break;
+ case 133: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 5711e33e..2f840a9b 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -551,6 +551,8 @@ namespace Microsoft.Boogie {
cce.EndExpose();
}
}
+
+ public HashSet<Variable> parallelCallLhss = new HashSet<Variable>();
}
public class TypecheckingContext : CheckingContext {
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index 873a5724..fded8dea 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer {
public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 94;
- const int noSym = 94;
+ const int maxT = 95;
+ const int noSym = 95;
[ContractInvariantMethod]
@@ -272,12 +272,12 @@ public class Scanner {
start[125] = 58;
start[61] = 59;
start[42] = 60;
+ start[124] = 61;
start[8660] = 28;
start[8658] = 30;
start[8656] = 31;
start[38] = 32;
start[8743] = 34;
- start[124] = 61;
start[8744] = 36;
start[33] = 62;
start[8800] = 40;
@@ -516,19 +516,19 @@ public class Scanner {
case "break": t.kind = 45; break;
case "assert": t.kind = 46; break;
case "assume": t.kind = 47; break;
- case "yield": t.kind = 48; break;
- case "havoc": t.kind = 49; break;
+ case "havoc": t.kind = 48; break;
+ case "yield": t.kind = 49; break;
case "async": t.kind = 51; break;
case "call": t.kind = 52; break;
- case "div": t.kind = 74; break;
- case "mod": t.kind = 75; break;
- case "false": t.kind = 80; break;
- case "true": t.kind = 81; break;
- case "old": t.kind = 82; break;
- case "then": t.kind = 85; break;
- case "forall": t.kind = 86; break;
- case "exists": t.kind = 88; break;
- case "lambda": t.kind = 90; break;
+ case "div": t.kind = 75; break;
+ case "mod": t.kind = 76; break;
+ case "false": t.kind = 81; break;
+ case "true": t.kind = 82; break;
+ case "old": t.kind = 83; break;
+ case "then": t.kind = 86; break;
+ case "forall": t.kind = 87; break;
+ case "exists": t.kind = 89; break;
+ case "lambda": t.kind = 91; break;
default: break;
}
}
@@ -650,62 +650,62 @@ public class Scanner {
case 26:
{t.kind = 50; break;}
case 27:
- {t.kind = 53; break;}
- case 28:
{t.kind = 54; break;}
- case 29:
+ case 28:
{t.kind = 55; break;}
- case 30:
+ case 29:
{t.kind = 56; break;}
+ case 30:
+ {t.kind = 57; break;}
case 31:
- {t.kind = 58; break;}
+ {t.kind = 59; break;}
case 32:
if (ch == '&') {AddCh(); goto case 33;}
else {goto case 0;}
case 33:
- {t.kind = 59; break;}
- case 34:
{t.kind = 60; break;}
- case 35:
+ case 34:
{t.kind = 61; break;}
- case 36:
+ case 35:
{t.kind = 62; break;}
+ case 36:
+ {t.kind = 63; break;}
case 37:
- {t.kind = 65; break;}
- case 38:
{t.kind = 66; break;}
- case 39:
+ case 38:
{t.kind = 67; break;}
- case 40:
+ case 39:
{t.kind = 68; break;}
- case 41:
+ case 40:
{t.kind = 69; break;}
- case 42:
+ case 41:
{t.kind = 70; break;}
- case 43:
+ case 42:
{t.kind = 71; break;}
+ case 43:
+ {t.kind = 72; break;}
case 44:
- {t.kind = 73; break;}
+ {t.kind = 74; break;}
case 45:
- {t.kind = 76; break;}
- case 46:
{t.kind = 77; break;}
+ case 46:
+ {t.kind = 78; break;}
case 47:
- {t.kind = 79; break;}
+ {t.kind = 80; break;}
case 48:
- {t.kind = 83; break;}
- case 49:
{t.kind = 84; break;}
+ case 49:
+ {t.kind = 85; break;}
case 50:
- {t.kind = 87; break;}
+ {t.kind = 88; break;}
case 51:
- {t.kind = 89; break;}
+ {t.kind = 90; break;}
case 52:
- {t.kind = 91; break;}
- case 53:
{t.kind = 92; break;}
- case 54:
+ case 53:
{t.kind = 93; break;}
+ case 54:
+ {t.kind = 94; break;}
case 55:
recEnd = pos; recKind = 11;
if (ch == '=') {AddCh(); goto case 26;}
@@ -733,29 +733,30 @@ public class Scanner {
if (ch == '*') {AddCh(); goto case 46;}
else {t.kind = 44; break;}
case 61:
+ recEnd = pos; recKind = 53;
if (ch == '|') {AddCh(); goto case 35;}
else if (ch == '{') {AddCh(); goto case 48;}
- else {goto case 0;}
+ else {t.kind = 53; break;}
case 62:
- recEnd = pos; recKind = 78;
+ recEnd = pos; recKind = 79;
if (ch == '=') {AddCh(); goto case 38;}
- else {t.kind = 78; break;}
+ else {t.kind = 79; break;}
case 63:
- recEnd = pos; recKind = 72;
+ recEnd = pos; recKind = 73;
if (ch == '+') {AddCh(); goto case 43;}
- else {t.kind = 72; break;}
+ else {t.kind = 73; break;}
case 64:
- recEnd = pos; recKind = 64;
+ recEnd = pos; recKind = 65;
if (ch == '=') {AddCh(); goto case 66;}
- else {t.kind = 64; break;}
+ else {t.kind = 65; break;}
case 65:
- recEnd = pos; recKind = 63;
+ recEnd = pos; recKind = 64;
if (ch == '>') {AddCh(); goto case 29;}
- else {t.kind = 63; break;}
+ else {t.kind = 64; break;}
case 66:
- recEnd = pos; recKind = 57;
+ recEnd = pos; recKind = 58;
if (ch == '>') {AddCh(); goto case 27;}
- else {t.kind = 57; break;}
+ else {t.kind = 58; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 2071154b..ee873bd4 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -84,13 +84,6 @@ namespace Microsoft.Boogie {
node.Expr = this.VisitExpr(node.Expr);
return node;
}
- public virtual Cmd VisitYieldCmd(YieldCmd node)
- {
- Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Cmd>() != null);
- node.Expr = this.VisitExpr(node.Expr);
- return node;
- }
public virtual AtomicRE VisitAtomicRE(AtomicRE node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<AtomicRE>() != null);
@@ -446,6 +439,12 @@ namespace Microsoft.Boogie {
Contract.Ensures(Contract.Result<ReturnCmd>() != null);
return (ReturnCmd)this.VisitTransferCmd(node);
}
+ public virtual YieldCmd VisitYieldCmd(YieldCmd node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<YieldCmd>() != null);
+ return node;
+ }
public virtual ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<ReturnExprCmd>() != null);
diff --git a/Test/og/Answer b/Test/og/Answer
index 712ebfd8..15dd93bd 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -1,9 +1,9 @@
-------------------- foo.bpl --------------------
-OwickiGriesDesugared.bpl(179,4): Error BP5001: This assertion might not hold.
+OwickiGriesDesugared.bpl(171,4): Error BP5001: This assertion might not hold.
Execution trace:
OwickiGriesDesugared.bpl(17,0): anon0
- OwickiGriesDesugared.bpl(177,0): inline$YieldChecker_PC$0$L1
+ OwickiGriesDesugared.bpl(169,0): inline$YieldChecker_PC$0$L1
Boogie program verifier finished with 3 verified, 1 error
@@ -23,6 +23,10 @@ Boogie program verifier finished with 2 verified, 2 errors
Boogie program verifier finished with 2 verified, 0 errors
+-------------------- parallel1.bpl --------------------
+
+Boogie program verifier finished with 4 verified, 0 errors
+
-------------------- linear-set.bpl --------------------
Boogie program verifier finished with 2 verified, 0 errors
@@ -38,3 +42,7 @@ Boogie program verifier finished with 3 verified, 0 errors
-------------------- DeviceCacheSimplified.bpl --------------------
Boogie program verifier finished with 5 verified, 0 errors
+
+-------------------- parallel2.bpl --------------------
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl
index c89bd793..68387356 100644
--- a/Test/og/DeviceCacheSimplified.bpl
+++ b/Test/og/DeviceCacheSimplified.bpl
@@ -13,7 +13,8 @@ ensures old(currsize) <= currsize;
ensures tid == tid';
{
assume tid == tid';
- assert {:yield} Inv(ghostLock, currsize, newsize);
+ yield;
+ assert Inv(ghostLock, currsize, newsize);
assert old(currsize) <= currsize;
assert tid != nil;
}
@@ -31,7 +32,8 @@ ensures currsize <= i;
ensures newsize == old(newsize);
{
assume tid == tid';
- assert {:yield} Inv(ghostLock, currsize, newsize);
+ yield;
+ assert Inv(ghostLock, currsize, newsize);
assert old(currsize) <= currsize;
assert tid != nil;
assert ghostLock == tid;
@@ -140,6 +142,6 @@ requires currsize == 0 && newsize == 0 && ghostLock == nil && lock == nil;
{
havoc tid;
assume tid != nil;
- call {:async} thread(tid);
+ async call thread(tid);
}
} \ No newline at end of file
diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 8379925f..217a0401 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -13,7 +13,7 @@ procedure {:entrypoint} main()
{
havoc tid, val;
assume tid != nil;
- call {:async} foo(tid, val);
+ async call foo(tid, val);
}
}
@@ -39,6 +39,7 @@ ensures tid == tid';
ensures old(l) == tid ==> old(l) == l && old(x) == x;
{
assume tid == tid';
- assert {:yield} tid != nil;
+ yield;
+ assert tid != nil;
assert (old(l) == tid ==> old(l) == l && old(x) == x);
} \ No newline at end of file
diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl
index cddc5338..8c4586d3 100644
--- a/Test/og/bar.bpl
+++ b/Test/og/bar.bpl
@@ -8,7 +8,8 @@ procedure PB()
procedure PC()
ensures g == old(g);
{
- assert{:yield} g == old(g);
+ yield;
+ assert g == old(g);
}
procedure PD()
@@ -22,8 +23,8 @@ procedure{:entrypoint} Main2()
{
while (true)
{
- call{:async} PB();
- call{:async} PC();
- call{:async} PD();
+ async call PB();
+ async call PC();
+ async call PD();
}
}
diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl
index d8d5bafd..776a165d 100644
--- a/Test/og/foo.bpl
+++ b/Test/og/foo.bpl
@@ -9,22 +9,23 @@ procedure PC()
ensures g == 3;
{
g := 3;
- assert{:yield} g == 3;
+ yield;
+ assert g == 3;
}
procedure PD()
{
call PC();
assert g == 3;
- assert{:yield} true;
+ yield;
}
procedure{:entrypoint} Main()
{
while (true)
{
- call{:async} PB();
- call{:async} PC();
- call{:async} PD();
+ async call PB();
+ async call PC();
+ async call PD();
}
}
diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index 04ad0df2..d188db3a 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -32,15 +32,16 @@ requires tidls' != None() && xls' == All();
assume tidls' == tidls && xls' == xls;
x := 42;
- assert {:yield} xls == All();
+ yield;
+ assert xls == All();
assert x == 42;
call xls1, xls2 := Split(xls);
havoc lsChild;
assume (lsChild != None());
- call {:async} thread(lsChild, xls1);
+ async call thread(lsChild, xls1);
havoc lsChild;
assume (lsChild != None());
- call {:async} thread(lsChild, xls2);
+ async call thread(lsChild, xls2);
}
procedure thread({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)
@@ -54,10 +55,13 @@ requires tidls' != None() && xls' != None();
assume l == None();
l := tidls;
- assert {:yield} tidls != None() && xls != None();
+ yield;
+ assert tidls != None() && xls != None();
x := 0;
- assert {:yield} tidls != None() && xls != None();
+ yield;
+ assert tidls != None() && xls != None();
assert x == 0;
- assert {:yield} tidls != None() && xls != None();
+ yield;
+ assert tidls != None() && xls != None();
l := None();
}
diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index 0df45254..5d627348 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -33,15 +33,16 @@ requires tidls' != nil && xls' == All();
assume tidls' == tidls && xls' == xls;
x := 42;
- assert {:yield} xls == All();
+ yield;
+ assert xls == All();
assert x == 42;
call xls1, xls2 := Split(xls);
havoc lsChild;
assume (lsChild != nil);
- call {:async} thread(lsChild, xls1);
+ async call thread(lsChild, xls1);
havoc lsChild;
assume (lsChild != nil);
- call {:async} thread(lsChild, xls2);
+ async call thread(lsChild, xls2);
}
procedure thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
@@ -55,10 +56,13 @@ requires tidls' != nil && xls' != None();
assume l == nil;
l := tidls;
- assert {:yield} tidls != nil && xls != None();
+ yield;
+ assert tidls != nil && xls != None();
x := 0;
- assert {:yield} tidls != nil && xls != None();
+ yield;
+ assert tidls != nil && xls != None();
assert x == 0;
- assert {:yield} tidls != nil && xls != None();
+ yield;
+ assert tidls != nil && xls != None();
l := nil;
}
diff --git a/Test/og/one.bpl b/Test/og/one.bpl
index bb7b1d01..806a4178 100644
--- a/Test/og/one.bpl
+++ b/Test/og/one.bpl
@@ -8,6 +8,7 @@ procedure A()
procedure B()
{
x := 5;
- assert{:yield} x == 5;
+ yield;
+ assert x == 5;
}
diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl
new file mode 100644
index 00000000..cb3502b4
--- /dev/null
+++ b/Test/og/parallel1.bpl
@@ -0,0 +1,29 @@
+var g:int;
+
+procedure PB()
+{
+ g := g + 1;
+}
+
+procedure PC()
+ ensures g == 3;
+{
+ g := 3;
+ yield;
+ assert g == 3;
+}
+
+procedure PD()
+{
+ call PC();
+ assert g == 3;
+ yield;
+}
+
+procedure{:entrypoint} Main()
+{
+ while (true)
+ {
+ call PB() | PC() | PD();
+ }
+}
diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
new file mode 100644
index 00000000..444b9805
--- /dev/null
+++ b/Test/og/parallel2.bpl
@@ -0,0 +1,35 @@
+var a:[int]int;
+
+procedure {:entrypoint} main()
+{
+ var {:linear "tid"} i: int;
+ var {:linear "tid"} j: int;
+ call i := t(i) | j := t(j);
+ call i := u(i) | j := u(j);
+}
+
+procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+{
+ assume i == i';
+
+ a[i] := 42;
+ call i := Yield(i);
+ assert a[i] == 42;
+}
+
+procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+{
+ assume i == i';
+
+ a[i] := 42;
+ yield;
+ assert a[i] == 42;
+}
+
+procedure Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+ensures i == i';
+ensures old(a)[i] == a[i];
+{
+ assume i == i';
+ yield;
+} \ No newline at end of file
diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index b00a3dda..0cca4898 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -3,13 +3,13 @@ setlocal
set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (foo.bpl bar.bpl one.bpl) do (
+for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
)
-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl) do (
+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
diff --git a/Test/prover/Answer b/Test/prover/Answer
index 688e6e6a..1ca6407c 100644
--- a/Test/prover/Answer
+++ b/Test/prover/Answer
@@ -4,7 +4,7 @@
z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
z3mutl.bpl(5,1): start
- z3mutl.bpl(8,1): L1
+ z3mutl.bpl(14,1): L3
z3mutl.bpl(20,1): L5
z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
@@ -14,7 +14,7 @@ Execution trace:
z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
z3mutl.bpl(5,1): start
- z3mutl.bpl(14,1): L3
+ z3mutl.bpl(8,1): L1
z3mutl.bpl(20,1): L5
Boogie program verifier finished with 0 verified, 3 errors
@@ -24,19 +24,19 @@ EQ_v2.Eval__v4.Eval_out.bpl(2101,5): Error BP5003: A postcondition might not hol
EQ_v2.Eval__v4.Eval_out.bpl(1715,3): Related location: This is the postcondition that might not hold.
Execution trace:
EQ_v2.Eval__v4.Eval_out.bpl(1786,3): AA_INSTR_EQ_BODY
- EQ_v2.Eval__v4.Eval_out.bpl(1875,3): inline$v2.Eval$0$label_11_case_1#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1862,3): inline$v2.Eval$0$label_11_case_2#2
EQ_v2.Eval__v4.Eval_out.bpl(1894,3): inline$v2.Eval$0$label_12#2
- EQ_v2.Eval__v4.Eval_out.bpl(2032,3): inline$v4.Eval$0$label_11_case_1#2
- EQ_v2.Eval__v4.Eval_out.bpl(2054,3): inline$v4.Eval$0$label_13_true#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1989,3): inline$v4.Eval$0$label_11_case_2#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2011,3): inline$v4.Eval$0$label_14_true#2
EQ_v2.Eval__v4.Eval_out.bpl(2081,3): inline$v4.Eval$0$label_12#2
EQ_v2.Eval__v4.Eval_out.bpl(2101,5): Error BP5003: A postcondition might not hold on this return path.
EQ_v2.Eval__v4.Eval_out.bpl(1715,3): Related location: This is the postcondition that might not hold.
Execution trace:
EQ_v2.Eval__v4.Eval_out.bpl(1786,3): AA_INSTR_EQ_BODY
- EQ_v2.Eval__v4.Eval_out.bpl(1862,3): inline$v2.Eval$0$label_11_case_2#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1875,3): inline$v2.Eval$0$label_11_case_1#2
EQ_v2.Eval__v4.Eval_out.bpl(1894,3): inline$v2.Eval$0$label_12#2
- EQ_v2.Eval__v4.Eval_out.bpl(1989,3): inline$v4.Eval$0$label_11_case_2#2
- EQ_v2.Eval__v4.Eval_out.bpl(2011,3): inline$v4.Eval$0$label_14_true#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2032,3): inline$v4.Eval$0$label_11_case_1#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2054,3): inline$v4.Eval$0$label_13_true#2
EQ_v2.Eval__v4.Eval_out.bpl(2081,3): inline$v4.Eval$0$label_12#2
EQ_v2.Eval__v4.Eval_out.bpl(2152,5): Error BP5003: A postcondition might not hold on this return path.
EQ_v2.Eval__v4.Eval_out.bpl(2120,3): Related location: This is the postcondition that might not hold.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 06:03:11 +0000