diff options
| author |  qadeer <unknown> | 2013-12-19 13:45:59 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2013-12-19 13:45:59 -0800 |
| commit | 2108194bc0fc2b69c3a5a738fc80b95900d50be6 (patch) | |
| tree | e0ca6d263178e11ec03a94698ba5b62a9c9d431d /Source/Core | |
| parent | 5524f179d2b3b89c2eaf7b4c913653dab48648ae (diff) | |
various updates and tighter integration of QED stuff into mainline
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Absy.cs | 20 | ||||
| -rw-r--r-- | Source/Core/Duplicator.cs | 24 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 12 |
3 files changed, 35 insertions, 21 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 6c333143..65de2297 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2351,14 +2351,22 @@ namespace Microsoft.Boogie { this.Condition.Resolve(rc);
}
+ public bool IsAtomicSpecification
+ {
+ get
+ {
+ return
+ QKeyValue.FindIntAttribute(this.Attributes, "atomic", int.MaxValue) != int.MaxValue ||
+ QKeyValue.FindIntAttribute(this.Attributes, "right", int.MaxValue) != int.MaxValue ||
+ QKeyValue.FindIntAttribute(this.Attributes, "left", int.MaxValue) != int.MaxValue ||
+ QKeyValue.FindIntAttribute(this.Attributes, "both", int.MaxValue) != int.MaxValue;
+ }
+ }
+
public override void Typecheck(TypecheckingContext tc) {
//Contract.Requires(tc != null);
- bool isAtomicSpecification =
- QKeyValue.FindIntAttribute(this.Attributes, "atomic", int.MaxValue) != int.MaxValue ||
- QKeyValue.FindIntAttribute(this.Attributes, "right", int.MaxValue) != int.MaxValue ||
- QKeyValue.FindIntAttribute(this.Attributes, "left", int.MaxValue) != int.MaxValue ||
- QKeyValue.FindIntAttribute(this.Attributes, "both", int.MaxValue) != int.MaxValue;
- if (isAtomicSpecification && !tc.Yields)
+
+ if (IsAtomicSpecification && !tc.Yields)
{
tc.Error(this, "atomic specification allowed only in a yielding procedure");
return;
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 056a47f9..0c49867c 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -113,15 +113,6 @@ namespace Microsoft.Boogie { clone.Outs = new List<IdentifierExpr>(clone.Outs);
return base.VisitCallCmd(clone);
}
- public override Cmd VisitParCallCmd(ParCallCmd node)
- {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Cmd>() != null);
- ParCallCmd clone = (ParCallCmd)node.Clone();
- Contract.Assert(clone != null);
- clone.CallCmds = new List<CallCmd>(node.CallCmds);
- return base.VisitParCallCmd(clone);
- }
public override Choice VisitChoice(Choice node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Choice>() != null);
@@ -251,6 +242,15 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Expr>() != null);
return base.VisitOldExpr((OldExpr)node.Clone());
}
+ public override Cmd VisitParCallCmd(ParCallCmd node)
+ {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
+ ParCallCmd clone = (ParCallCmd)node.Clone();
+ Contract.Assert(clone != null);
+ clone.CallCmds = new List<CallCmd>(node.CallCmds);
+ return base.VisitParCallCmd(clone);
+ }
public override Procedure VisitProcedure(Procedure node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Procedure>() != null);
@@ -352,6 +352,12 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Requires>() != null);
return base.VisitRequires((Requires)node.Clone());
}
+ public override YieldCmd VisitYieldCmd(YieldCmd node)
+ {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Requires>() != null);
+ return base.VisitYieldCmd((YieldCmd)node.Clone());
+ }
}
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index cd59638b..4605019f 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -468,12 +468,6 @@ 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);
@@ -588,6 +582,12 @@ namespace Microsoft.Boogie { }
return variableSeq;
}
+ public virtual YieldCmd VisitYieldCmd(YieldCmd node)
+ {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<YieldCmd>() != null);
+ return node;
+ }
public virtual Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
|