diff options
Diffstat (limited to 'Source/Core/AbsyCmd.cs')
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 2047 |
1 files changed, 1232 insertions, 815 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 7aa3e1fc..e31348a1 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -7,34 +7,42 @@ // BoogiePL - Absy.cs
//---------------------------------------------------------------------------------------------
-namespace Microsoft.Boogie
-{
+namespace Microsoft.Boogie {
using System;
using System.Collections;
using System.Diagnostics;
using System.Collections.Generic;
using Microsoft.Boogie.AbstractInterpretation;
using AI = Microsoft.AbstractInterpretationFramework;
- using Microsoft.Contracts;
+ using System.Diagnostics.Contracts;
//---------------------------------------------------------------------
// BigBlock
- public class BigBlock
- {
- public readonly IToken! tok;
+ public class BigBlock {
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(tok != null);
+ Contract.Invariant(Anonymous || LabelName != null);
+ Contract.Invariant(ec == null || tc == null);
+ Contract.Invariant(simpleCmds != null);
+ }
+
+ public readonly IToken/*!*/ tok;
public string LabelName;
public readonly bool Anonymous;
- invariant !Anonymous ==> LabelName != null;
- [Rep] public CmdSeq! simpleCmds;
+
+ [Rep]
+ public CmdSeq/*!*/ simpleCmds;
public StructuredCmd ec;
public TransferCmd tc;
- invariant ec == null || tc == null;
+
public BigBlock successorBigBlock; // null if successor is end of proceduure body (or if field has not yet been initialized)
- public BigBlock(IToken! tok, string? labelName, [Captured] CmdSeq! simpleCmds, StructuredCmd? ec, TransferCmd? tc)
- requires ec == null || tc == null;
- {
+ public BigBlock(IToken tok, string labelName, [Captured] CmdSeq simpleCmds, StructuredCmd ec, TransferCmd tc) {
+ Contract.Requires(simpleCmds != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(ec == null || tc == null);
this.tok = tok;
this.LabelName = labelName;
this.Anonymous = labelName == null;
@@ -43,45 +51,57 @@ namespace Microsoft.Boogie this.tc = tc;
}
- public void Emit(TokenTextWriter! stream, int level) {
+ public void Emit(TokenTextWriter stream, int level) {
+ Contract.Requires(stream != null);
if (!Anonymous) {
- stream.WriteLine(level, "{0}:",
+ stream.WriteLine(level, "{0}:",
CommandLineOptions.Clo.PrintWithUniqueASTIds ? String.Format("h{0}^^{1}", this.GetHashCode(), this.LabelName) : this.LabelName);
}
- foreach (Cmd! c in this.simpleCmds) {
- c.Emit(stream, level+1);
+ foreach (Cmd/*!*/ c in this.simpleCmds) {
+ Contract.Assert(c != null);
+ c.Emit(stream, level + 1);
}
if (this.ec != null) {
- this.ec.Emit(stream, level+1);
+ this.ec.Emit(stream, level + 1);
} else if (this.tc != null) {
- this.tc.Emit(stream, level+1);
+ this.tc.Emit(stream, level + 1);
}
}
}
- public class StmtList
- {
- [Rep] public readonly List<BigBlock!>! BigBlocks;
+ public class StmtList {
+ [Rep]
+ public readonly List<BigBlock/*!*/>/*!*/ BigBlocks;
public CmdSeq PrefixCommands;
- public readonly IToken! EndCurly;
+ public readonly IToken/*!*/ EndCurly;
public StmtList ParentContext;
public BigBlock ParentBigBlock;
- public Set<string!>! Labels = new Set<string!>();
+ public Set<string/*!*/>/*!*/ Labels = new Set<string/*!*/>();
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(EndCurly != null);
+ Contract.Invariant(cce.NonNullElements(BigBlocks));
+ Contract.Invariant(cce.NonNullElements(Labels));
+ }
- public StmtList([Captured] List<BigBlock!>! bigblocks, IToken! endCurly)
- requires bigblocks.Count > 0;
- {
+
+ public StmtList([Captured] List<BigBlock/*!*/>/*!*/ bigblocks, IToken endCurly) {
+ Contract.Requires(endCurly != null);
+ Contract.Requires(cce.NonNullElements(bigblocks));
+ Contract.Requires(bigblocks.Count > 0);
this.BigBlocks = bigblocks;
this.EndCurly = endCurly;
}
// prints the list of statements, not the surrounding curly braces
- public void Emit(TokenTextWriter! stream, int level) {
+ public void Emit(TokenTextWriter stream, int level) {
+ Contract.Requires(stream != null);
bool needSeperator = false;
foreach (BigBlock b in BigBlocks) {
- assume b.IsPeerConsistent;
+ Contract.Assert(b != null);
+ Contract.Assume(cce.IsPeerConsistent(b));
if (needSeperator) {
stream.WriteLine();
}
@@ -101,10 +121,11 @@ namespace Microsoft.Boogie /// Note, to be conservative (that is, ignoring the possible optimization that this
/// method enables), this method can do nothing and return false.
/// </summary>
- public bool PrefixFirstBlock([Captured] CmdSeq! prefixCmds, ref string! suggestedLabel)
- ensures !result ==> Owner.None(prefixCmds); // "prefixCmds" is captured only on success
- {
- assume PrefixCommands == null; // prefix has not been used
+ public bool PrefixFirstBlock([Captured] CmdSeq prefixCmds, ref string suggestedLabel) {
+ Contract.Requires(suggestedLabel != null);
+ Contract.Requires(prefixCmds != null);
+ Contract.Ensures(Contract.Result<bool>() || cce.Owner.None(prefixCmds)); // "prefixCmds" is captured only on success
+ Contract.Assume(PrefixCommands == null); // prefix has not been used
BigBlock bb0 = BigBlocks[0];
if (prefixCmds.Length == 0) {
@@ -113,7 +134,7 @@ namespace Microsoft.Boogie if (bb0.Anonymous) {
bb0.LabelName = suggestedLabel;
} else {
- assert bb0.LabelName != null;
+ Contract.Assert(bb0.LabelName != null);
suggestedLabel = bb0.LabelName;
}
return true;
@@ -138,14 +159,17 @@ namespace Microsoft.Boogie /// The StmtListBuilder class makes it easier to build structured commands.
/// </summary>
public class StmtListBuilder {
- List<BigBlock!>! bigBlocks = new List<BigBlock!>();
+ List<BigBlock/*!*/>/*!*/ bigBlocks = new List<BigBlock/*!*/>();
string label;
CmdSeq simpleCmds;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(bigBlocks));
+ }
- void Dump(StructuredCmd scmd, TransferCmd tcmd)
- requires scmd == null || tcmd == null;
- ensures label == null && simpleCmds == null;
- {
+ void Dump(StructuredCmd scmd, TransferCmd tcmd) {
+ Contract.Requires(scmd == null || tcmd == null);
+ Contract.Ensures(label == null && simpleCmds == null);
if (label == null && simpleCmds == null && scmd == null && tcmd == null) {
// nothing to do
} else {
@@ -162,7 +186,9 @@ namespace Microsoft.Boogie /// Collects the StmtList built so far and returns it. The StmtListBuilder should no longer
/// be used once this method has been invoked.
/// </summary>
- public StmtList! Collect(IToken! endCurlyBrace) {
+ public StmtList Collect(IToken endCurlyBrace) {
+ Contract.Requires(endCurlyBrace != null);
+ Contract.Ensures(Contract.Result<StmtList>() != null);
Dump(null, null);
if (bigBlocks.Count == 0) {
simpleCmds = new CmdSeq(); // the StmtList constructor doesn't like an empty list of BigBlock's
@@ -171,48 +197,66 @@ namespace Microsoft.Boogie return new StmtList(bigBlocks, endCurlyBrace);
}
- public void Add(Cmd! cmd) {
+ public void Add(Cmd cmd) {
+ Contract.Requires(cmd != null);
if (simpleCmds == null) {
simpleCmds = new CmdSeq();
}
simpleCmds.Add(cmd);
}
- public void Add(StructuredCmd! scmd) {
+ public void Add(StructuredCmd scmd) {
+ Contract.Requires(scmd != null);
Dump(scmd, null);
}
- public void Add(TransferCmd! tcmd) {
+ public void Add(TransferCmd tcmd) {
+ Contract.Requires(tcmd != null);
Dump(null, tcmd);
}
- public void AddLabelCmd(string! label) {
+ public void AddLabelCmd(string label) {
+ Contract.Requires(label != null);
Dump(null, null);
this.label = label;
}
- public void AddLocalVariable(string! name) {
+ public void AddLocalVariable(string name) {
+ Contract.Requires(name != null);
// TODO
}
}
class BigBlocksResolutionContext {
- StmtList! stmtList;
- [Peer] List<Block!> blocks;
- string! prefix = "anon";
+ StmtList/*!*/ stmtList;
+ [Peer]
+ List<Block/*!*/> blocks;
+ string/*!*/ prefix = "anon";
int anon = 0;
- Set<string!> allLabels = new Set<string!>();
- Errors! errorHandler;
+ Set<string/*!*/> allLabels = new Set<string/*!*/>();
+ Errors/*!*/ errorHandler;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(stmtList != null);
+ Contract.Invariant(cce.NonNullElements(blocks, true));
+ Contract.Invariant(prefix != null);
+ Contract.Invariant(cce.NonNullElements(allLabels, true));
+ Contract.Invariant(errorHandler != null);
+ }
- public BigBlocksResolutionContext(StmtList! stmtList, Errors! errorHandler) {
+
+ public BigBlocksResolutionContext(StmtList stmtList, Errors errorHandler) {
+ Contract.Requires(errorHandler != null);
+ Contract.Requires(stmtList != null);
this.stmtList = stmtList;
this.errorHandler = errorHandler;
}
- public List<Block!>! Blocks {
+ public List<Block/*!*/>/*!*/ Blocks {
get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
if (blocks == null) {
- blocks = new List<Block!>();
+ blocks = new List<Block/*!*/>();
int startErrorCount = this.errorHandler.count;
// Check that there are no goto's into the middle of a block, and no break statement to a non-enclosing loop.
@@ -234,12 +278,12 @@ namespace Microsoft.Boogie }
}
- void CheckLegalLabels(StmtList! stmtList, StmtList parentContext, BigBlock parentBigBlock)
- requires parentContext == null <==> parentBigBlock == null;
- requires stmtList.ParentContext == null; // it hasn't been set yet
- modifies stmtList.*;
- ensures stmtList.ParentContext == parentContext;
- {
+ void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parentBigBlock) {
+ Contract.Requires(stmtList != null);
+ Contract.Requires((parentContext == null) == (parentBigBlock == null));
+ Contract.Requires(stmtList.ParentContext == null); // it hasn't been set yet
+ //modifies stmtList.*;
+ Contract.Ensures(stmtList.ParentContext == parentContext);
stmtList.ParentContext = parentContext;
stmtList.ParentBigBlock = parentBigBlock;
@@ -263,7 +307,8 @@ namespace Microsoft.Boogie // goto's must reference blocks in enclosing blocks
if (b.tc is GotoCmd) {
GotoCmd g = (GotoCmd)b.tc;
- foreach (string! lbl in (!)g.labelNames) {
+ foreach (string/*!*/ lbl in cce.NonNull(g.labelNames)) {
+ Contract.Assert(lbl != null);
bool found = false;
for (StmtList sl = stmtList; sl != null; sl = sl.ParentContext) {
if (sl.Labels.Contains(lbl)) {
@@ -280,11 +325,10 @@ namespace Microsoft.Boogie // break labels must refer to an enclosing while statement
else if (b.ec is BreakCmd) {
BreakCmd bcmd = (BreakCmd)b.ec;
- assert bcmd.BreakEnclosure == null; // it hasn't been initialized yet
+ Contract.Assert(bcmd.BreakEnclosure == null); // it hasn't been initialized yet
bool found = false;
- for (StmtList sl = stmtList; sl.ParentBigBlock != null; sl = sl.ParentContext)
- invariant sl != null;
- {
+ for (StmtList sl = stmtList; sl.ParentBigBlock != null; sl = sl.ParentContext) {
+ cce.LoopInvariant(sl != null);
BigBlock bb = sl.ParentBigBlock;
if (bcmd.Label == null) {
@@ -331,7 +375,8 @@ namespace Microsoft.Boogie }
}
- void NameAnonymousBlocks(StmtList! stmtList) {
+ void NameAnonymousBlocks(StmtList stmtList) {
+ Contract.Requires(stmtList != null);
foreach (BigBlock b in stmtList.BigBlocks) {
if (b.LabelName == null) {
b.LabelName = prefix + anon;
@@ -351,7 +396,8 @@ namespace Microsoft.Boogie }
}
- void RecordSuccessors(StmtList! stmtList, BigBlock successor) {
+ void RecordSuccessors(StmtList stmtList, BigBlock successor) {
+ Contract.Requires(stmtList != null);
for (int i = stmtList.BigBlocks.Count; 0 <= --i; ) {
BigBlock big = stmtList.BigBlocks[i];
big.successorBigBlock = successor;
@@ -374,15 +420,15 @@ namespace Microsoft.Boogie // If the enclosing context is a loop, then "runOffTheEndLabel" is the loop head label;
// otherwise, it is null.
- void CreateBlocks(StmtList! stmtList, string runOffTheEndLabel)
- requires blocks != null;
- {
+ void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) {
+ Contract.Requires(stmtList != null);
+ Contract.Requires(blocks != null);
CmdSeq cmdPrefixToApply = stmtList.PrefixCommands;
int n = stmtList.BigBlocks.Count;
foreach (BigBlock b in stmtList.BigBlocks) {
n--;
- assert b.LabelName != null;
+ Contract.Assert(b.LabelName != null);
CmdSeq theSimpleCmds;
if (cmdPrefixToApply == null) {
theSimpleCmds = b.simpleCmds;
@@ -395,7 +441,7 @@ namespace Microsoft.Boogie if (b.tc != null) {
// this BigBlock has the very same components as a Block
- assert b.ec == null;
+ Contract.Assert(b.ec == null);
Block block = new Block(b.tok, b.LabelName, theSimpleCmds, b.tc);
blocks.Add(block);
@@ -412,14 +458,14 @@ namespace Microsoft.Boogie } else if (b.ec is BreakCmd) {
BreakCmd bcmd = (BreakCmd)b.ec;
- assert bcmd.BreakEnclosure != null;
+ Contract.Assert(bcmd.BreakEnclosure != null);
Block block = new Block(b.tok, b.LabelName, theSimpleCmds, GotoSuccessor(b.ec.tok, bcmd.BreakEnclosure));
blocks.Add(block);
} else if (b.ec is WhileCmd) {
WhileCmd wcmd = (WhileCmd)b.ec;
string loopHeadLabel = prefix + anon + "_LoopHead";
- string! loopBodyLabel = prefix + anon + "_LoopBody";
+ string/*!*/ loopBodyLabel = prefix + anon + "_LoopBody";
string loopDoneLabel = prefix + anon + "_LoopDone";
anon++;
@@ -471,8 +517,10 @@ namespace Microsoft.Boogie CmdSeq predCmds = theSimpleCmds;
for (; ifcmd != null; ifcmd = ifcmd.elseIf) {
- string! thenLabel = prefix + anon + "_Then";
- string! elseLabel = prefix + anon + "_Else";
+ string thenLabel = prefix + anon + "_Then";
+ Contract.Assert(thenLabel != null);
+ string elseLabel = prefix + anon + "_Else";
+ Contract.Assert(elseLabel != null);
anon++;
CmdSeq ssThen = new CmdSeq();
@@ -504,7 +552,7 @@ namespace Microsoft.Boogie CreateBlocks(ifcmd.thn, n == 0 ? runOffTheEndLabel : null);
if (ifcmd.elseBlock != null) {
- assert ifcmd.elseIf == null;
+ Contract.Assert(ifcmd.elseIf == null);
if (!elseGuardTakenCareOf) {
// Else: assume !guard; goto firstElseBlock;
block = new Block(ifcmd.tok, elseLabel, ssElse, new GotoCmd(ifcmd.tok, new StringSeq(ifcmd.elseBlock.BigBlocks[0].LabelName)));
@@ -540,7 +588,10 @@ namespace Microsoft.Boogie }
}
- TransferCmd! GotoSuccessor(IToken! tok, BigBlock! b) {
+ TransferCmd GotoSuccessor(IToken tok, BigBlock b) {
+ Contract.Requires(b != null);
+ Contract.Requires(tok != null);
+ Contract.Ensures(Contract.Result<TransferCmd>() != null);
if (b.successorBigBlock != null) {
return new GotoCmd(tok, new StringSeq(b.successorBigBlock.LabelName));
} else {
@@ -549,29 +600,50 @@ namespace Microsoft.Boogie }
}
- public abstract class StructuredCmd
- {
- public IToken! tok;
- public StructuredCmd(IToken! tok)
- {
+ [ContractClass(typeof(StructuredCmdContracts))]
+ public abstract class StructuredCmd {
+ public IToken/*!*/ tok;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(tok != null);
+ }
+
+ public StructuredCmd(IToken tok) {
+ Contract.Requires(tok != null);
this.tok = tok;
}
- public abstract void Emit(TokenTextWriter! stream, int level);
+ public abstract void Emit(TokenTextWriter/*!*/ stream, int level);
}
+ [ContractClassFor(typeof(StructuredCmd))]
+ public abstract class StructuredCmdContracts : StructuredCmd {
+ public override void Emit(TokenTextWriter stream, int level) {
+ Contract.Requires(stream != null);
+ throw new NotImplementedException();
+ }
+ public StructuredCmdContracts() :base(null){
- public class IfCmd : StructuredCmd
- {
- public Expr? Guard;
- public StmtList! thn;
- public IfCmd? elseIf;
+ }
+ }
+
+ public class IfCmd : StructuredCmd {
+ public Expr Guard;
+ public StmtList/*!*/ thn;
+ public IfCmd elseIf;
public StmtList elseBlock;
- invariant elseIf == null || elseBlock == null;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(thn != null);
+ Contract.Invariant(elseIf == null || elseBlock == null);
+ }
+
- public IfCmd(IToken! tok, Expr? guard, StmtList! thn, IfCmd? elseIf, StmtList elseBlock)
- : base(tok)
- requires elseIf == null || elseBlock == null;
- {
+
+ public IfCmd(IToken/*!*/ tok, Expr guard, StmtList/*!*/ thn, IfCmd elseIf, StmtList elseBlock)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(thn != null);
+ Contract.Requires(elseIf == null || elseBlock == null);
this.Guard = guard;
this.thn = thn;
this.elseIf = elseIf;
@@ -579,9 +651,9 @@ namespace Microsoft.Boogie // base(tok);
}
- public override void Emit(TokenTextWriter! stream, int level) {
+ public override void Emit(TokenTextWriter stream, int level) {
stream.Write(level, "if (");
- IfCmd! ifcmd = this;
+ IfCmd/*!*/ ifcmd = this;
while (true) {
if (ifcmd.Guard == null) {
stream.Write("*");
@@ -609,22 +681,30 @@ namespace Microsoft.Boogie }
}
- public class WhileCmd : StructuredCmd
- {
- [Peer] public Expr? Guard;
- public List<PredicateCmd!>! Invariants;
- public StmtList! Body;
+ public class WhileCmd : StructuredCmd {
+ [Peer]
+ public Expr Guard;
+ public List<PredicateCmd/*!*/>/*!*/ Invariants;
+ public StmtList/*!*/ Body;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Body != null);
+ Contract.Invariant(cce.NonNullElements(Invariants));
+ }
+
- public WhileCmd(IToken! tok, [Captured] Expr? guard, List<PredicateCmd!>! invariants, StmtList! body)
- : base(tok)
- {
+ public WhileCmd(IToken tok, [Captured] Expr guard, List<PredicateCmd/*!*/>/*!*/ invariants, StmtList/*!*/ body)
+ : base(tok) {
+ Contract.Requires(cce.NonNullElements(invariants));
+ Contract.Requires(body != null);
+ Contract.Requires(tok != null);
this.Guard = guard;
this.Invariants = invariants;
this.Body = body;
/// base(tok);
}
- public override void Emit(TokenTextWriter! stream, int level) {
+ public override void Emit(TokenTextWriter stream, int level) {
stream.Write(level, "while (");
if (Guard == null) {
stream.Write("*");
@@ -649,19 +729,19 @@ namespace Microsoft.Boogie }
}
- public class BreakCmd : StructuredCmd
- {
+ public class BreakCmd : StructuredCmd {
public string Label;
public BigBlock BreakEnclosure;
- public BreakCmd(IToken! tok, string? label)
- : base(tok)
- {
+ public BreakCmd(IToken tok, string label)
+ : base(tok) {
+ Contract.Requires(tok != null);
this.Label = label;
// base(tok);
}
- public override void Emit(TokenTextWriter! stream, int level) {
+ public override void Emit(TokenTextWriter stream, int level) {
+
if (Label == null) {
stream.WriteLine(level, "break;");
} else {
@@ -672,10 +752,11 @@ namespace Microsoft.Boogie //---------------------------------------------------------------------
// Block
- public sealed class Block : Absy
- {
- public string! Label; // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
- [Rep] [ElementsPeer] public CmdSeq! Cmds;
+ public sealed class Block : Absy {
+ public string/*!*/ Label; // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
+ [Rep]
+ [ElementsPeer]
+ public CmdSeq/*!*/ Cmds;
[Rep] //PM: needed to verify Traverse.Visit
public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures)
@@ -683,7 +764,11 @@ namespace Microsoft.Boogie // public bool currentlyTraversed;
- public enum VisitState {ToVisit, BeingVisited, AlreadyVisited}; // used by WidenPoints.Compute
+ public enum VisitState {
+ ToVisit,
+ BeingVisited,
+ AlreadyVisited
+ }; // used by WidenPoints.Compute
public VisitState TraversingStatus;
public bool widenBlock;
@@ -693,22 +778,38 @@ namespace Microsoft.Boogie public AI.Lattice Lattice; // The lattice used for the analysis of this block
public AI.Lattice.Element PreInvariant; // The initial abstract states for this block
public AI.Lattice.Element PostInvariant; // The exit abstract states for this block
- // KRML: We want to include the following invariant, but at the moment, doing so causes a run-time error (something about committed): invariant PreInvariant != null <==> PostInvariant != null;
+ // KRML: We want to include the following invariant, but at the moment, doing so causes a run-time error (something about committed):
+ //invariant ;
// VC generation and SCC computation
- public BlockSeq! Predecessors;
+ public BlockSeq/*!*/ Predecessors;
- public Set<Variable!> liveVarsBefore;
- public bool IsLive(Variable! v) {
- if (liveVarsBefore == null) return true;
+ public Set<Variable/*!*/> liveVarsBefore;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Label != null);
+ Contract.Invariant(Cmds != null);
+ Contract.Invariant(cce.NonNullElements(liveVarsBefore, true));
+ Contract.Invariant((PreInvariant != null) == (PostInvariant != null));
+ }
+
+ public bool IsLive(Variable v) {
+ Contract.Requires(v != null);
+ if (liveVarsBefore == null)
+ return true;
return liveVarsBefore.Contains(v);
}
-
- public Block() { this(Token.NoToken, "", new CmdSeq(), new ReturnCmd(Token.NoToken));}
- public Block (IToken! tok, string! label, CmdSeq! cmds, TransferCmd transferCmd)
- : base(tok)
- {
+ public Block()
+ : this(Token.NoToken, "", new CmdSeq(), new ReturnCmd(Token.NoToken)) {
+
+ }
+
+ public Block(IToken tok, string/*!*/ label, CmdSeq/*!*/ cmds, TransferCmd transferCmd)
+ : base(tok) {
+ Contract.Requires(label != null);
+ Contract.Requires(cmds != null);
+ Contract.Requires(tok != null);
this.Label = label;
this.Cmds = cmds;
this.TransferCmd = transferCmd;
@@ -721,8 +822,8 @@ namespace Microsoft.Boogie // base(tok);
}
- public void Emit (TokenTextWriter! stream, int level)
- {
+ public void Emit(TokenTextWriter stream, int level) {
+ Contract.Requires(stream != null);
stream.WriteLine();
stream.WriteLine(
this,
@@ -731,45 +832,45 @@ namespace Microsoft.Boogie CommandLineOptions.Clo.PrintWithUniqueASTIds ? String.Format("h{0}^^{1}", this.GetHashCode(), this.Label) : this.Label,
this.widenBlock ? " // cut point" : "");
- foreach (Cmd! c in this.Cmds)
- {
+ foreach (Cmd/*!*/ c in this.Cmds) {
+ Contract.Assert(c != null);
c.Emit(stream, level + 1);
}
- assume this.TransferCmd != null;
+ Contract.Assume(this.TransferCmd != null);
this.TransferCmd.Emit(stream, level + 1);
}
- public void Register (ResolutionContext! rc)
- {
+ public void Register(ResolutionContext rc) {
+ Contract.Requires(rc != null);
rc.AddBlock(this);
}
- public override void Resolve (ResolutionContext! rc)
- {
- foreach (Cmd! c in Cmds)
- {
+ public override void Resolve(ResolutionContext rc) {
+
+
+ foreach (Cmd/*!*/ c in Cmds) {
+ Contract.Assert(c != null);
c.Resolve(rc);
}
- assume this.TransferCmd != null;
+ Contract.Assume(this.TransferCmd != null);
TransferCmd.Resolve(rc);
}
- public override void Typecheck (TypecheckingContext! tc)
- {
- foreach (Cmd! c in Cmds)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+
+ foreach (Cmd/*!*/ c in Cmds) {
+ Contract.Assert(c != null);
c.Typecheck(tc);
}
- assume this.TransferCmd != null;
+ Contract.Assume(this.TransferCmd != null);
TransferCmd.Typecheck(tc);
}
/// <summary>
/// Reset the abstract intepretation state of this block. It does this by putting the iterations to 0 and the pre and post states to null
/// </summary>
- public void ResetAbstractInterpretationState()
- {
-// this.currentlyTraversed = false;
+ public void ResetAbstractInterpretationState() {
+ // this.currentlyTraversed = false;
this.TraversingStatus = VisitState.ToVisit;
this.iterations = 0;
this.Lattice = null;
@@ -778,89 +879,119 @@ namespace Microsoft.Boogie }
[Pure]
- public override string! ToString()
- {
- return this.Label + (this.widenBlock? "[w]" : "");
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return this.Label + (this.widenBlock ? "[w]" : "");
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitBlock(this);
}
}
//---------------------------------------------------------------------
// Commands
+ [ContractClassFor(typeof(Cmd))]
+ public abstract class CmdContracts : Cmd {
+ public CmdContracts() :base(null){
- public abstract class Cmd : Absy
- {
- public Cmd(IToken! tok) : base(tok) { }
- public abstract void Emit(TokenTextWriter! stream, int level);
- public abstract void AddAssignedVariables(VariableSeq! vars);
- public void CheckAssignments(TypecheckingContext! tc)
- {
- VariableSeq! vars = new VariableSeq();
+ }
+ public override void Emit(TokenTextWriter stream, int level) {
+ Contract.Requires(stream != null);
+ throw new NotImplementedException();
+ }
+ public override void AddAssignedVariables(VariableSeq vars) {
+ Contract.Requires(vars != null);
+ throw new NotImplementedException();
+ }
+ }
+ [ContractClass(typeof(CmdContracts))]
+ public abstract class Cmd : Absy {
+ public Cmd(IToken/*!*/ tok)
+ : base(tok) {
+ Contract.Assert(tok != null);
+ }
+ 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)
- {
- if (!v.IsMutable)
- {
+ 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 (v is GlobalVariable && !tc.InFrame(v))
- {
+ } else if (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
- public static AssignCmd! SimpleAssign(IToken! tok, IdentifierExpr! lhs, Expr! rhs) {
- List<AssignLhs!>! lhss = new List<AssignLhs!> ();
- List<Expr!>! rhss = new List<Expr!> ();
-
- lhss.Add(new SimpleAssignLhs (lhs.tok, lhs));
+ public static AssignCmd SimpleAssign(IToken tok, IdentifierExpr lhs, Expr rhs) {
+ Contract.Requires(rhs != null);
+ Contract.Requires(lhs != null);
+ Contract.Requires(tok != null);
+ Contract.Ensures(Contract.Result<AssignCmd>() != null);
+ List<AssignLhs/*!*/>/*!*/ lhss = new List<AssignLhs/*!*/>();
+ List<Expr/*!*/>/*!*/ rhss = new List<Expr/*!*/>();
+
+ lhss.Add(new SimpleAssignLhs(lhs.tok, lhs));
rhss.Add(rhs);
return new AssignCmd(tok, lhss, rhss);
}
- public static AssignCmd! MapAssign(IToken! tok,
- IdentifierExpr! map,
- ExprSeq! indexes, Expr! rhs) {
- List<AssignLhs!>! lhss = new List<AssignLhs!> ();
- List<Expr!>! rhss = new List<Expr!> ();
- List<Expr!>! indexesList = new List<Expr!> ();
+ public static AssignCmd/*!*/ MapAssign(IToken tok,
+ IdentifierExpr/*!*/ map,
+ ExprSeq/*!*/ indexes, Expr/*!*/ rhs) {
+
+ Contract.Requires(tok != null);
+ Contract.Requires(map != null);
+ Contract.Requires(indexes != null);
+ Contract.Requires(rhs != null);
+ Contract.Ensures(Contract.Result<AssignCmd>() != null);
+ List<AssignLhs/*!*/>/*!*/ lhss = new List<AssignLhs/*!*/>();
+ List<Expr/*!*/>/*!*/ rhss = new List<Expr/*!*/>();
+ List<Expr/*!*/>/*!*/ indexesList = new List<Expr/*!*/>();
+
+
foreach (Expr e in indexes)
- indexesList.Add((!)e);
+ indexesList.Add(cce.NonNull(e));
- lhss.Add(new MapAssignLhs (map.tok,
- new SimpleAssignLhs (map.tok, map),
+ lhss.Add(new MapAssignLhs(map.tok,
+ new SimpleAssignLhs(map.tok, map),
indexesList));
rhss.Add(rhs);
return new AssignCmd(tok, lhss, rhss);
}
- public static AssignCmd! MapAssign(IToken! tok,
- IdentifierExpr! map,
- params Expr[]! args)
- requires args.Length > 0; // at least the rhs
- requires forall{int i in (0:args.Length); args[i] != null};
- {
- List<AssignLhs!>! lhss = new List<AssignLhs!> ();
- List<Expr!>! rhss = new List<Expr!> ();
- List<Expr!>! indexesList = new List<Expr!> ();
+ public static AssignCmd/*!*/ MapAssign(IToken tok,
+ IdentifierExpr/*!*/ map,
+ params Expr[]/*!*/ args) {
+ Contract.Requires(tok != null);
+ Contract.Requires(map != null);
+ Contract.Requires(args != null);
+ Contract.Requires(args.Length > 0); // at least the rhs
+ Contract.Requires(Contract.ForAll(args, i => i != null));
+ Contract.Ensures(Contract.Result<AssignCmd>() != null);
+
+ List<AssignLhs/*!*/>/*!*/ lhss = new List<AssignLhs/*!*/>();
+ List<Expr/*!*/>/*!*/ rhss = new List<Expr/*!*/>();
+ List<Expr/*!*/>/*!*/ indexesList = new List<Expr/*!*/>();
for (int i = 0; i < args.Length - 1; ++i)
- indexesList.Add((!)args[i]);
+ indexesList.Add(cce.NonNull(args[i]));
- lhss.Add(new MapAssignLhs (map.tok,
- new SimpleAssignLhs (map.tok, map),
+ lhss.Add(new MapAssignLhs(map.tok,
+ new SimpleAssignLhs(map.tok, map),
indexesList));
- rhss.Add((!)args[args.Length - 1]);
-
+ rhss.Add(cce.NonNull(args[args.Length - 1]));
+
return new AssignCmd(tok, lhss, rhss);
}
@@ -868,21 +999,21 @@ namespace Microsoft.Boogie /// This is a helper routine for printing a linked list of attributes. Each attribute
/// is terminated by a space.
/// </summary>
- public static void EmitAttributes(TokenTextWriter! stream, QKeyValue attributes)
- {
+ public static void EmitAttributes(TokenTextWriter stream, QKeyValue attributes) {
+ Contract.Requires(stream != null);
for (QKeyValue kv = attributes; kv != null; kv = kv.Next) {
kv.Emit(stream);
stream.Write(" ");
}
}
- public static void ResolveAttributes(QKeyValue attributes, ResolutionContext! rc)
- {
+ public static void ResolveAttributes(QKeyValue attributes, ResolutionContext rc) {
+ Contract.Requires(rc != null);
for (QKeyValue kv = attributes; kv != null; kv = kv.Next) {
kv.Resolve(rc);
}
}
- public static void TypecheckAttributes(QKeyValue attributes, TypecheckingContext! tc)
- {
+ public static void TypecheckAttributes(QKeyValue attributes, TypecheckingContext tc) {
+ Contract.Requires(tc != null);
for (QKeyValue kv = attributes; kv != null; kv = kv.Next) {
kv.Typecheck(tc);
}
@@ -891,27 +1022,39 @@ namespace Microsoft.Boogie public class CommentCmd : Cmd // just a convenience for debugging
{
- public readonly string! Comment;
- public CommentCmd (string! c)
- : base(Token.NoToken)
- {
+ public readonly string/*!*/ Comment;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Comment != null);
+ }
+
+ public CommentCmd(string c)
+ : base(Token.NoToken) {
+ Contract.Requires(c != null);
Comment = c;
// base(Token.NoToken);
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+
if (this.Comment.Contains("\n")) {
stream.WriteLine(this, level, "/* {0} */", this.Comment);
} else {
stream.WriteLine(this, level, "// {0}", this.Comment);
}
}
- public override void Resolve(ResolutionContext! rc) { }
- public override void AddAssignedVariables(VariableSeq! vars) { }
- public override void Typecheck(TypecheckingContext! tc) { }
+ public override void Resolve(ResolutionContext rc) {
+
+ }
+ public override void AddAssignedVariables(VariableSeq vars) {
+
+ }
+ public override void Typecheck(TypecheckingContext tc) {
+
+ }
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+
+
return visitor.VisitCommentCmd(this);
}
}
@@ -919,21 +1062,32 @@ namespace Microsoft.Boogie // class for parallel assignments, which subsumes both the old
// SimpleAssignCmd and the old MapAssignCmd
public class AssignCmd : Cmd {
- public List<AssignLhs!>! Lhss;
- public List<Expr!>! Rhss;
+ public List<AssignLhs/*!*/>/*!*/ Lhss;
+ public List<Expr/*!*/>/*!*/ Rhss;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(Lhss));
+ Contract.Invariant(cce.NonNullElements(Rhss));
+ }
- public AssignCmd(IToken! tok, List<AssignLhs!>! lhss, List<Expr!>! rhss) {
- base(tok);
+
+ public AssignCmd(IToken tok, List<AssignLhs/*!*/>/*!*/ lhss, List<Expr/*!*/>/*!*/ rhss)
+ : base(tok) {//BASEMOVEA
+ Contract.Requires(tok != null);
+ Contract.Requires(cce.NonNullElements(rhss));
+ Contract.Requires(cce.NonNullElements(lhss));
+ //base(tok);
Lhss = lhss;
Rhss = rhss;
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+
stream.Write(this, level, "");
- string! sep = "";
- foreach (AssignLhs! l in Lhss) {
+ string/*!*/ sep = "";
+ foreach (AssignLhs/*!*/ l in Lhss) {
+ Contract.Assert(l != null);
stream.Write(sep);
sep = ", ";
l.Emit(stream);
@@ -942,7 +1096,8 @@ namespace Microsoft.Boogie stream.Write(" := ");
sep = "";
- foreach (Expr! e in Rhss) {
+ foreach (Expr/*!*/ e in Rhss) {
+ Contract.Assert(e != null);
stream.Write(sep);
sep = ", ";
e.Emit(stream);
@@ -951,22 +1106,26 @@ namespace Microsoft.Boogie stream.WriteLine(";");
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+
if (Lhss.Count != Rhss.Count)
rc.Error(this,
"number of left-hand sides does not match number of right-hand sides");
- foreach (AssignLhs! e in Lhss)
+ foreach (AssignLhs/*!*/ e in Lhss) {
+ Contract.Assert(e != null);
e.Resolve(rc);
- foreach (Expr! e in Rhss)
+ }
+ foreach (Expr/*!*/ e in Rhss) {
+ Contract.Assert(e != null);
e.Resolve(rc);
+ }
// check for double occurrences of assigned variables
// (could be optimised)
for (int i = 0; i < Lhss.Count; ++i) {
for (int j = i + 1; j < Lhss.Count; ++j) {
- if (((!)Lhss[i].DeepAssignedVariable).Equals(
+ if (cce.NonNull(Lhss[i].DeepAssignedVariable).Equals(
Lhss[j].DeepAssignedVariable))
rc.Error(Lhss[j],
"variable {0} is assigned more than once in parallel assignment",
@@ -975,11 +1134,16 @@ namespace Microsoft.Boogie }
}
- public override void Typecheck(TypecheckingContext! tc) {
- foreach (AssignLhs! e in Lhss)
+ public override void Typecheck(TypecheckingContext tc) {
+
+ foreach (AssignLhs/*!*/ e in Lhss) {
+ Contract.Assert(e != null);
e.Typecheck(tc);
- foreach (Expr! e in Rhss)
+ }
+ foreach (Expr/*!*/ e in Rhss) {
+ Contract.Assert(e != null);
e.Typecheck(tc);
+ }
this.CheckAssignments(tc);
@@ -997,97 +1161,169 @@ namespace Microsoft.Boogie }
}
- public override void AddAssignedVariables(VariableSeq! vars)
- {
- foreach (AssignLhs! l in Lhss)
+ public override void AddAssignedVariables(VariableSeq vars) {
+
+ foreach (AssignLhs/*!*/ l in Lhss) {
+ Contract.Assert(l != null);
vars.Add(l.DeepAssignedVariable);
+ }
}
// transform away the syntactic sugar of map assignments and
// determine an equivalent assignment in which all rhs are simple
// variables
- public AssignCmd! AsSimpleAssignCmd { get {
- List<AssignLhs!>! newLhss = new List<AssignLhs!> ();
- List<Expr!>! newRhss = new List<Expr!> ();
-
- for (int i = 0; i < Lhss.Count; ++i) {
- IdentifierExpr! newLhs;
- Expr! newRhs;
- Lhss[i].AsSimpleAssignment(Rhss[i], out newLhs, out newRhs);
- newLhss.Add(new SimpleAssignLhs(Token.NoToken, newLhs));
- newRhss.Add(newRhs);
+ public AssignCmd/*!*/ AsSimpleAssignCmd {
+ get {
+ Contract.Ensures(Contract.Result<AssignCmd>() != null);
+
+ List<AssignLhs/*!*/>/*!*/ newLhss = new List<AssignLhs/*!*/>();
+ List<Expr/*!*/>/*!*/ newRhss = new List<Expr/*!*/>();
+
+ for (int i = 0; i < Lhss.Count; ++i) {
+ IdentifierExpr/*!*/ newLhs;
+ Expr/*!*/ newRhs;
+ Lhss[i].AsSimpleAssignment(Rhss[i], out newLhs, out newRhs);
+ newLhss.Add(new SimpleAssignLhs(Token.NoToken, newLhs));
+ newRhss.Add(newRhs);
+ }
+
+ return new AssignCmd(Token.NoToken, newLhss, newRhss);
}
+ }
- return new AssignCmd(Token.NoToken, newLhss, newRhss);
- } }
+ public override Absy StdDispatch(StandardVisitor visitor) {
+
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
return visitor.VisitAssignCmd(this);
}
}
// There are two different kinds of left-hand sides in assignments:
// simple variables (identifiers), or locations of a map
+ [ContractClass(typeof(AssignLhsContracts))]
public abstract class AssignLhs : Absy {
// The type of the lhs is determined during typechecking
- public abstract Type Type { get; }
+ public abstract Type Type {
+ get;
+ }
// Determine the variable that is actually assigned in this lhs
- public abstract IdentifierExpr! DeepAssignedIdentifier { get; }
- public abstract Variable DeepAssignedVariable { get; }
+ public abstract IdentifierExpr/*!*/ DeepAssignedIdentifier {
+ get;
+ }
+ public abstract Variable DeepAssignedVariable {
+ get;
+ }
- public AssignLhs(IToken! tok) : base(tok) {}
- public abstract void Emit(TokenTextWriter! stream);
+ public AssignLhs(IToken/*!*/ tok)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ }
+ public abstract void Emit(TokenTextWriter/*!*/ stream);
- public abstract Expr! AsExpr { get; }
+ public abstract Expr/*!*/ AsExpr {
+ get;
+ }
// transform away the syntactic sugar of map assignments and
// determine an equivalent simple assignment
- internal abstract void AsSimpleAssignment(Expr! rhs,
- out IdentifierExpr! simpleLhs,
- out Expr! simpleRhs);
+ internal abstract void AsSimpleAssignment(Expr/*!*/ rhs,
+ out IdentifierExpr/*!*/ simpleLhs,
+ out Expr/*!*/ simpleRhs);
+ }
+ [ContractClassFor(typeof(AssignLhs))]
+ public abstract class AssignLhsContracts : AssignLhs {
+ public AssignLhsContracts():base(null)
+ {
+
+ }public override IdentifierExpr DeepAssignedIdentifier {
+
+ get {
+ Contract.Ensures(Contract.Result<IdentifierExpr>() != null);
+ throw new NotImplementedException();
+ }
+ }
+ public override Expr AsExpr {
+ get {
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ throw new NotImplementedException();
+ }
+
+ }
+ internal override void AsSimpleAssignment(Expr rhs, out IdentifierExpr simpleLhs, out Expr simpleRhs) {
+ Contract.Requires(rhs != null);
+ Contract.Ensures(Contract.ValueAtReturn(out simpleLhs) != null);
+ Contract.Ensures(Contract.ValueAtReturn(out simpleRhs) != null);
+
+ throw new NotImplementedException();
+ }
}
public class SimpleAssignLhs : AssignLhs {
- public IdentifierExpr! AssignedVariable;
+ public IdentifierExpr/*!*/ AssignedVariable;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(AssignedVariable != null);
+ }
- public override Type Type { get {
- return AssignedVariable.Type;
- } }
- public override IdentifierExpr! DeepAssignedIdentifier { get {
- return AssignedVariable;
- } }
+ public override Type Type {
+ get {
+ return AssignedVariable.Type;
+ }
+ }
+
+ public override IdentifierExpr/*!*/ DeepAssignedIdentifier {
+ get {
+ Contract.Ensures(Contract.Result<IdentifierExpr>() != null);
+ return AssignedVariable;
+ }
+ }
- public override Variable DeepAssignedVariable { get {
- return AssignedVariable.Decl;
- } }
+ public override Variable DeepAssignedVariable {
+ get {
+ return AssignedVariable.Decl;
+ }
+ }
- public SimpleAssignLhs(IToken! tok, IdentifierExpr! assignedVariable) {
- base(tok);
+ public SimpleAssignLhs(IToken tok, IdentifierExpr assignedVariable)
+ : base(tok) {
+ Contract.Requires(assignedVariable != null);
+ Contract.Requires(tok != null);
+ //base(tok);
AssignedVariable = assignedVariable;
}
- public override void Resolve(ResolutionContext! rc) {
+ public override void Resolve(ResolutionContext rc) {
+
AssignedVariable.Resolve(rc);
}
- public override void Typecheck(TypecheckingContext! tc) {
+ public override void Typecheck(TypecheckingContext tc) {
+
AssignedVariable.Typecheck(tc);
}
- public override void Emit(TokenTextWriter! stream) {
+ public override void Emit(TokenTextWriter stream) {
+
AssignedVariable.Emit(stream);
}
- public override Expr! AsExpr { get {
- return AssignedVariable;
- } }
- internal override void AsSimpleAssignment(Expr! rhs,
- out IdentifierExpr! simpleLhs,
- out Expr! simpleRhs) {
+ public override Expr/*!*/ AsExpr {
+ get {
+ Contract.Ensures(Contract.Result<Expr>() != null);
+
+ return AssignedVariable;
+ }
+ }
+ internal override void AsSimpleAssignment(Expr rhs,
+ out IdentifierExpr/*!*/ simpleLhs,
+ out Expr/*!*/ simpleRhs) {
+
+
+
simpleLhs = AssignedVariable;
simpleRhs = rhs;
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+
+
return visitor.VisitSimpleAssignLhs(this);
}
}
@@ -1096,9 +1332,15 @@ namespace Microsoft.Boogie // a map select expression, but it is cleaner to keep those two
// things separate
public class MapAssignLhs : AssignLhs {
- public AssignLhs! Map;
+ public AssignLhs/*!*/ Map;
+
+ public List<Expr/*!*/>/*!*/ Indexes;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Map != null);
+ Contract.Invariant(cce.NonNullElements(Indexes));
+ }
- public List<Expr!>! Indexes;
// The instantiation of type parameters of the map that is
// determined during type checking.
@@ -1106,69 +1348,102 @@ namespace Microsoft.Boogie private Type TypeAttr = null;
- public override Type Type { get {
- return TypeAttr;
- } }
+ public override Type Type {
+ get {
+ return TypeAttr;
+ }
+ }
+
+ public override IdentifierExpr/*!*/ DeepAssignedIdentifier {
+ get {
+ Contract.Ensures(Contract.Result<IdentifierExpr>() != null);
- public override IdentifierExpr! DeepAssignedIdentifier { get {
- return Map.DeepAssignedIdentifier;
- } }
+ return Map.DeepAssignedIdentifier;
+ }
+ }
+
+ public override Variable DeepAssignedVariable {
+ get {
+ return Map.DeepAssignedVariable;
+ }
+ }
- public override Variable DeepAssignedVariable { get {
- return Map.DeepAssignedVariable;
- } }
+ public MapAssignLhs(IToken tok, AssignLhs map, List<Expr/*!*/>/*!*/ indexes)
+ : base(tok) {//BASEMOVEA
+ //:base(tok);
+ Contract.Requires(map != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(cce.NonNullElements(indexes));
- public MapAssignLhs(IToken! tok, AssignLhs! map, List<Expr!>! indexes) {
- base(tok);
Map = map;
Indexes = indexes;
}
- public override void Resolve(ResolutionContext! rc) {
+ public override void Resolve(ResolutionContext rc) {
+
Map.Resolve(rc);
- foreach (Expr! e in Indexes)
+ foreach (Expr/*!*/ e in Indexes) {
+ Contract.Assert(e != null);
e.Resolve(rc);
+ }
}
- public override void Typecheck(TypecheckingContext! tc) {
+ public override void Typecheck(TypecheckingContext tc) {
+
Map.Typecheck(tc);
- foreach (Expr! e in Indexes)
+ foreach (Expr/*!*/ e in Indexes) {
+ Contract.Assert(e != null);
e.Typecheck(tc);
+ }
// we use the same typechecking code as in MapSelect
- ExprSeq! selectArgs = new ExprSeq ();
- foreach (Expr! e in Indexes)
+ ExprSeq/*!*/ selectArgs = new ExprSeq();
+ foreach (Expr/*!*/ e in Indexes) {
+ Contract.Assert(e != null);
selectArgs.Add(e);
- TypeParamInstantiation! tpInsts;
+ }
+ TypeParamInstantiation/*!*/ tpInsts;
TypeAttr =
- MapSelect.Typecheck((!)Map.Type, Map,
+ MapSelect.Typecheck(cce.NonNull(Map.Type), Map,
selectArgs, out tpInsts, tc, tok, "map assignment");
TypeParameters = tpInsts;
}
- public override void Emit(TokenTextWriter! stream) {
+ public override void Emit(TokenTextWriter stream) {
+
Map.Emit(stream);
stream.Write("[");
- string! sep = "";
- foreach (Expr! e in Indexes) {
+ string/*!*/ sep = "";
+ foreach (Expr/*!*/ e in Indexes) {
+ Contract.Assert(e != null);
stream.Write(sep);
sep = ", ";
e.Emit(stream);
}
stream.Write("]");
}
- public override Expr! AsExpr { get {
- NAryExpr! res = Expr.Select(Map.AsExpr, Indexes);
- res.TypeParameters = this.TypeParameters;
- return res;
- } }
- internal override void AsSimpleAssignment(Expr! rhs,
- out IdentifierExpr! simpleLhs,
- out Expr! simpleRhs) {
- NAryExpr! newRhs = Expr.Store(Map.AsExpr, Indexes, rhs);
+ public override Expr/*!*/ AsExpr {
+ get {
+ Contract.Ensures(Contract.Result<Expr>() != null);
+
+ NAryExpr/*!*/ res = Expr.Select(Map.AsExpr, Indexes);
+ Contract.Assert(res != null);
+ res.TypeParameters = this.TypeParameters;
+ return res;
+ }
+ }
+ internal override void AsSimpleAssignment(Expr rhs,
+ out IdentifierExpr/*!*/ simpleLhs,
+ out Expr/*!*/ simpleRhs) { //Contract.Requires(rhs != null);
+ Contract.Ensures(Contract.ValueAtReturn(out simpleLhs) != null);
+ Contract.Ensures(Contract.ValueAtReturn(out simpleRhs) != null);
+
+ NAryExpr/*!*/ newRhs = Expr.Store(Map.AsExpr, Indexes, rhs);
+ Contract.Assert(newRhs != null);
newRhs.TypeParameters = this.TypeParameters;
Map.AsSimpleAssignment(newRhs, out simpleLhs, out simpleRhs);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitMapAssignLhs(this);
}
}
@@ -1178,90 +1453,111 @@ namespace Microsoft.Boogie /// There is no user syntax for a StateCmd. Instead, a StateCmd is only used
/// temporarily during the desugaring phase inside the VC generator.
/// </summary>
- public class StateCmd : Cmd
- {
- public /*readonly, except for the StandardVisitor*/ VariableSeq! Locals;
- public /*readonly, except for the StandardVisitor*/ CmdSeq! Cmds;
-
- public StateCmd(IToken! tok, VariableSeq! locals, CmdSeq! cmds)
- : base(tok)
- {
- this.Locals = locals;
- this.Cmds = cmds;
- // base(tok);
+ public class StateCmd : Cmd {
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Locals != null);
+ Contract.Invariant(Cmds != null);
+ }
+
+ public /*readonly, except for the StandardVisitor*/ VariableSeq/*!*/ Locals;
+ public /*readonly, except for the StandardVisitor*/ CmdSeq/*!*/ Cmds;
+
+ public StateCmd(IToken tok, VariableSeq/*!*/ locals, CmdSeq/*!*/ cmds)
+ : base(tok) {
+ Contract.Requires(locals != null);
+ Contract.Requires(cmds != null);
+ Contract.Requires(tok != null);
+ this.Locals = locals;
+ this.Cmds = cmds;
+ // base(tok);
}
- public override void Resolve(ResolutionContext! rc) {
- rc.PushVarContext();
- foreach (Variable! v in Locals) {
- rc.AddVariable(v, false);
- }
- foreach (Cmd! cmd in Cmds) {
- cmd.Resolve(rc);
- }
- rc.PopVarContext();
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ rc.PushVarContext();
+ foreach (Variable/*!*/ v in Locals) {
+ Contract.Assert(v != null);
+ rc.AddVariable(v, false);
+ }
+ foreach (Cmd/*!*/ cmd in Cmds) {
+ Contract.Assert(cmd != null);
+ cmd.Resolve(rc);
+ }
+ rc.PopVarContext();
}
- public override void AddAssignedVariables(VariableSeq! vars) {
- VariableSeq! vs = new VariableSeq();
- foreach (Cmd! cmd in this.Cmds)
- {
- cmd.AddAssignedVariables(vs);
- }
- System.Collections.Hashtable! localsSet = new System.Collections.Hashtable();
- foreach (Variable! local in this.Locals)
- {
- localsSet[local] = bool.TrueString;
- }
- foreach (Variable! v in vs)
- {
- if (!localsSet.ContainsKey(v))
- {
- vars.Add(v);
- }
+ public override void AddAssignedVariables(VariableSeq vars) {
+ //Contract.Requires(vars != null);
+ VariableSeq/*!*/ vs = new VariableSeq();
+ foreach (Cmd/*!*/ cmd in this.Cmds) {
+ Contract.Assert(cmd != null);
+ cmd.AddAssignedVariables(vs);
+ }
+ System.Collections.Hashtable/*!*/ localsSet = new System.Collections.Hashtable();
+ foreach (Variable/*!*/ local in this.Locals) {
+ Contract.Assert(local != null);
+ localsSet[local] = bool.TrueString;
+ }
+ foreach (Variable/*!*/ v in vs) {
+ Contract.Assert(v != null);
+ if (!localsSet.ContainsKey(v)) {
+ vars.Add(v);
}
+ }
}
- public override void Typecheck(TypecheckingContext! tc) {
- foreach (Cmd! cmd in Cmds) {
- cmd.Typecheck(tc);
- }
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ foreach (Cmd/*!*/ cmd in Cmds) {
+ Contract.Assert(cmd != null);
+ cmd.Typecheck(tc);
+ }
}
- public override void Emit(TokenTextWriter! stream, int level) {
- stream.WriteLine(this, level, "{");
- foreach (Variable! v in Locals) {
- v.Emit(stream, level+1);
- }
- foreach (Cmd! c in Cmds) {
- c.Emit(stream, level+1);
- }
- stream.WriteLine(level, "}");
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
+ stream.WriteLine(this, level, "{");
+ foreach (Variable/*!*/ v in Locals) {
+ Contract.Assert(v != null);
+ v.Emit(stream, level + 1);
+ }
+ foreach (Cmd/*!*/ c in Cmds) {
+ Contract.Assert(c != null);
+ c.Emit(stream, level + 1);
+ }
+ stream.WriteLine(level, "}");
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitStateCmd(this);
}
}
-
- abstract public class SugaredCmd : Cmd
- {
+ [ContractClass(typeof(SugaredCmdContracts))]
+ abstract public class SugaredCmd : Cmd {
private Cmd desugaring; // null until desugared
- public SugaredCmd(IToken! tok) : base(tok) {}
+ public SugaredCmd(IToken/*!*/ tok)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ }
+
+ public Cmd/*!*/ Desugaring {
+ get {
+ Contract.Ensures(Contract.Result<Cmd>() != null);
- public Cmd! Desugaring {
- get {
- if (desugaring == null) {
- desugaring = ComputeDesugaring();
- }
- return desugaring;
+ if (desugaring == null) {
+ desugaring = ComputeDesugaring();
}
+ return desugaring;
+ }
}
- protected abstract Cmd! ComputeDesugaring();
+ protected abstract Cmd/*!*/ ComputeDesugaring();
- public override void Emit(TokenTextWriter! stream, int level) {
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
if (CommandLineOptions.Clo.PrintDesugarings) {
stream.WriteLine(this, level, "/*** desugaring:");
Desugaring.Emit(stream, level);
@@ -1269,21 +1565,41 @@ namespace Microsoft.Boogie }
}
}
+ [ContractClassFor(typeof(SugaredCmd))]
+ public abstract class SugaredCmdContracts : SugaredCmd {
+ public SugaredCmdContracts() :base(null){
- public abstract class CallCommonality : SugaredCmd
- {
+ }
+ protected override Cmd ComputeDesugaring() {
+ Contract.Ensures(Contract.Result<Cmd>() != null);
+
+ throw new NotImplementedException();
+ }
+ }
+
+ public abstract class CallCommonality : SugaredCmd {
public QKeyValue Attributes;
-
- protected CallCommonality(IToken! tok, QKeyValue kv) {
- base(tok);
+
+ protected CallCommonality(IToken tok, QKeyValue kv)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ //base(tok);
Attributes = kv;
}
- protected enum TempVarKind { Formal, Old, Bound }
-
+ protected enum TempVarKind {
+ Formal,
+ Old,
+ Bound
+ }
+
// We have to give the type explicitly, because the type of the formal "likeThisOne" can contain type variables
- protected Variable! CreateTemporaryVariable(VariableSeq! tempVars, Variable! likeThisOne, Type! ty, TempVarKind kind) {
- string! tempNamePrefix;
+ protected Variable CreateTemporaryVariable(VariableSeq tempVars, Variable likeThisOne, Type ty, TempVarKind kind) {
+ Contract.Requires(ty != null);
+ Contract.Requires(likeThisOne != null);
+ Contract.Requires(tempVars != null);
+ Contract.Ensures(Contract.Result<Variable>() != null);
+ string/*!*/ tempNamePrefix;
switch (kind) {
case TempVarKind.Formal:
tempNamePrefix = "formal@";
@@ -1294,31 +1610,39 @@ namespace Microsoft.Boogie case TempVarKind.Bound:
tempNamePrefix = "forall@";
break;
- default:
- assert false; // unexpected kind
+ default: {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // unexpected kind
}
TypedIdent ti = likeThisOne.TypedIdent;
TypedIdent newTi = new TypedIdent(ti.tok, "call" + UniqueId + tempNamePrefix + ti.Name, ty);
- Variable! v;
+ Variable/*!*/ v;
if (kind == TempVarKind.Bound) {
v = new BoundVariable(likeThisOne.tok, newTi);
} else {
v = new LocalVariable(likeThisOne.tok, newTi);
tempVars.Add(v);
- }
+ }
return v;
}
}
- public class CallCmd : CallCommonality, IPotentialErrorNode
- {
- string! callee;
+ public class CallCmd : CallCommonality, IPotentialErrorNode {
+ string/*!*/ callee;
public Procedure Proc;
// Element of the following lists can be null, which means that
// the call happens with * as these parameters
- public List<Expr>! Ins;
- public List<IdentifierExpr>! Outs;
+ public List<Expr>/*!*/ Ins;
+ public List<IdentifierExpr>/*!*/ Outs;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(callee != null);
+ Contract.Invariant(Ins != null);
+ Contract.Invariant(Outs != null);
+ }
+
//public Lattice.Element StateAfterCall;
// The instantiation of type parameters that is determined during
@@ -1328,52 +1652,70 @@ namespace Microsoft.Boogie // TODO: convert to use generics
private object errorData;
public object ErrorData {
- get { return errorData; }
- set { errorData = value; }
- }
-
- public CallCmd(IToken! tok, string! callee, ExprSeq! ins, IdentifierExprSeq! outs)
- {
- List<Expr>! insList = new List<Expr> ();
- List<IdentifierExpr>! outsList = new List<IdentifierExpr> ();
- foreach (Expr e in ins)
- insList.Add(e);
- foreach (IdentifierExpr e in outs)
- outsList.Add(e);
-
- this(tok, callee, insList, outsList);
- }
- public CallCmd(IToken! tok, string! callee, List<Expr>! ins, List<IdentifierExpr>! outs)
- {
- base(tok, null);
+ get {
+ return errorData;
+ }
+ set {
+ errorData = value;
+ }
+ }
+
+ public CallCmd(IToken tok, string callee, ExprSeq ins, IdentifierExprSeq outs)
+ : this(tok, callee, cce.toList<Expr>(ins), cce.toList<IdentifierExpr>(outs)) {
+ Contract.Requires(outs != null);
+ Contract.Requires(ins != null);
+ Contract.Requires(callee != null);
+ Contract.Requires(tok != null);
+ //List<Expr>/*!*/ insList = new List<Expr>();
+ //List<IdentifierExpr>/*!*/ outsList = new List<IdentifierExpr>();
+ //foreach (Expr e in ins)
+ // if(e!=null)
+ // insList.Add(e);
+ //foreach (IdentifierExpr e in outs)
+ // if(e!=null)
+ // outsList.Add(e);
+ //this(tok, callee, insList, outsList);
+
+ }
+ public CallCmd(IToken tok, string callee, List<Expr> ins, List<IdentifierExpr> outs)
+ : base(tok, null) {//BASEMOVE DANGER
+ Contract.Requires(outs != null);
+ Contract.Requires(ins != null);
+ Contract.Requires(callee != null);
+ Contract.Requires(tok != null);
+ //base(tok, null);
this.callee = callee;
this.Ins = ins;
this.Outs = outs;
}
- public CallCmd(IToken! tok, string! callee, List<Expr>! ins, List<IdentifierExpr>! outs, QKeyValue kv)
- {
- base(tok, kv);
+ public CallCmd(IToken tok, string callee, List<Expr> ins, List<IdentifierExpr> outs, QKeyValue kv)
+ : base(tok, kv) {//BASEMOVE DANGER
+ Contract.Requires(outs != null);
+ Contract.Requires(ins != null);
+ Contract.Requires(callee != null);
+ Contract.Requires(tok != null);
+ //base(tok, kv);
this.callee = callee;
this.Ins = ins;
this.Outs = outs;
}
-
- public override void Emit(TokenTextWriter! stream, int level)
- {
+
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
stream.Write(this, level, "call ");
EmitAttributes(stream, Attributes);
string sep = "";
if (Outs.Count > 0) {
- foreach (Expr arg in Outs) {
- stream.Write(sep);
- sep = ", ";
- if (arg == null) {
- stream.Write("*");
- } else {
- arg.Emit(stream);
- }
- }
- stream.Write(" := ");
+ foreach (Expr arg in Outs) {
+ stream.Write(sep);
+ sep = ", ";
+ if (arg == null) {
+ stream.Write("*");
+ } else {
+ arg.Emit(stream);
+ }
+ }
+ stream.Write(" := ");
}
stream.Write(TokenTextWriter.SanitizeIdentifier(callee));
stream.Write("(");
@@ -1390,10 +1732,9 @@ namespace Microsoft.Boogie stream.WriteLine(");");
base.Emit(stream, level);
}
- public override void Resolve(ResolutionContext! rc)
- {
- if (Proc != null)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ if (Proc != null) {
// already resolved
return;
}
@@ -1402,15 +1743,13 @@ namespace Microsoft.Boogie if (Proc == null) {
rc.Error(this, "call to undeclared procedure: {0}", callee);
}
- foreach (Expr e in Ins)
- {
- if (e!=null) {
+ foreach (Expr e in Ins) {
+ if (e != null) {
e.Resolve(rc);
}
}
Set/*<Variable>*/ actualOuts = new Set/*<Variable>*/ (Outs.Count);
- foreach (IdentifierExpr ide in Outs)
- {
+ foreach (IdentifierExpr ide in Outs) {
if (ide != null) {
ide.Resolve(rc);
if (ide.Decl != null) {
@@ -1447,27 +1786,29 @@ namespace Microsoft.Boogie rc.Error(this.tok, "a procedure called asynchronously can have at most one output parameter");
return;
}
- }
-
+ }
+
// Check that type parameters can be determined using the given
// actual i/o arguments. This is done already during resolution
// because CheckBoundVariableOccurrences needs a resolution
// context
- TypeSeq! formalInTypes = new TypeSeq();
- TypeSeq! formalOutTypes = new TypeSeq();
+ TypeSeq/*!*/ formalInTypes = new TypeSeq();
+ TypeSeq/*!*/ formalOutTypes = new TypeSeq();
for (int i = 0; i < Ins.Count; ++i)
if (Ins[i] != null)
- formalInTypes.Add(((!)Proc.InParams[i]).TypedIdent.Type);
+ formalInTypes.Add(cce.NonNull(Proc.InParams[i]).TypedIdent.Type);
for (int i = 0; i < Outs.Count; ++i)
if (Outs[i] != null)
- formalOutTypes.Add(((!)Proc.OutParams[i]).TypedIdent.Type);
-
+ formalOutTypes.Add(cce.NonNull(Proc.OutParams[i]).TypedIdent.Type);
+
// we need to bind the type parameters for this
// (this is expected by CheckBoundVariableOccurrences)
int previousTypeBinderState = rc.TypeBinderState;
try {
- foreach (TypeVariable! v in Proc.TypeParameters)
+ foreach (TypeVariable/*!*/ v in Proc.TypeParameters) {
+ Contract.Assert(v != null);
rc.AddTypeBinder(v);
+ }
Type.CheckBoundVariableOccurrences(Proc.TypeParameters,
formalInTypes, formalOutTypes,
this.tok, "types of given arguments",
@@ -1477,66 +1818,62 @@ namespace Microsoft.Boogie }
}
- public override void AddAssignedVariables(VariableSeq! vars)
- {
- foreach (IdentifierExpr e in Outs)
- {
- if (e!=null) {
+ public override void AddAssignedVariables(VariableSeq vars) {
+ //Contract.Requires(vars != null);
+ foreach (IdentifierExpr e in Outs) {
+ if (e != null) {
vars.Add(e.Decl);
}
}
- assume this.Proc != null;
- foreach (IdentifierExpr! e in this.Proc.Modifies)
- {
+ Contract.Assume(this.Proc != null);
+ foreach (IdentifierExpr/*!*/ e in this.Proc.Modifies) {
+ Contract.Assert(e != null);
vars.Add(e.Decl);
}
}
- public override void Typecheck(TypecheckingContext! tc)
- {
- assume this.Proc != null; // we assume the CallCmd has been successfully resolved before calling this Typecheck method
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ Contract.Assume(this.Proc != null); // we assume the CallCmd has been successfully resolved before calling this Typecheck method
TypecheckAttributes(Attributes, tc);
// typecheck in-parameters
foreach (Expr e in Ins)
- if (e!=null)
+ if (e != null)
e.Typecheck(tc);
foreach (Expr e in Outs)
- if (e!=null)
+ if (e != null)
e.Typecheck(tc);
this.CheckAssignments(tc);
- TypeSeq! formalInTypes = new TypeSeq();
- TypeSeq! formalOutTypes = new TypeSeq();
- ExprSeq! actualIns = new ExprSeq();
- IdentifierExprSeq! actualOuts = new IdentifierExprSeq();
- for (int i = 0; i < Ins.Count; ++i)
- {
+ TypeSeq/*!*/ formalInTypes = new TypeSeq();
+ TypeSeq/*!*/ formalOutTypes = new TypeSeq();
+ ExprSeq/*!*/ actualIns = new ExprSeq();
+ IdentifierExprSeq/*!*/ actualOuts = new IdentifierExprSeq();
+ for (int i = 0; i < Ins.Count; ++i) {
if (Ins[i] != null) {
- formalInTypes.Add(((!)Proc.InParams[i]).TypedIdent.Type);
+ formalInTypes.Add(cce.NonNull(Proc.InParams[i]).TypedIdent.Type);
actualIns.Add(Ins[i]);
}
- }
- for (int i = 0; i < Outs.Count; ++i)
- {
+ }
+ for (int i = 0; i < Outs.Count; ++i) {
if (Outs[i] != null) {
- formalOutTypes.Add(((!)Proc.OutParams[i]).TypedIdent.Type);
+ formalOutTypes.Add(cce.NonNull(Proc.OutParams[i]).TypedIdent.Type);
actualOuts.Add(Outs[i]);
}
}
-
+
if (QKeyValue.FindBoolAttribute(this.Attributes, "async") && Outs.Count > 0) {
- Type returnType = ((!)Outs[0]).ShallowType;
- if (!returnType.Equals(Type.Int))
- {
+ Type returnType = cce.NonNull(Outs[0]).ShallowType;
+ if (!returnType.Equals(Type.Int)) {
tc.Error(this.tok, "the return from an asynchronous call should be an integer");
return;
}
}
-
+
// match actuals with formals
- List<Type!>! actualTypeParams;
+ List<Type/*!*/>/*!*/ actualTypeParams;
Type.CheckArgumentTypes(Proc.TypeParameters,
out actualTypeParams,
formalInTypes, actualIns,
@@ -1544,28 +1881,33 @@ namespace Microsoft.Boogie this.tok,
"call to " + callee,
tc);
+ Contract.Assert(cce.NonNullElements(actualTypeParams));
TypeParameters = SimpleTypeParamInstantiation.From(Proc.TypeParameters,
actualTypeParams);
}
- private IDictionary<TypeVariable!, Type!>! TypeParamSubstitution() {
- assume TypeParameters != null;
- IDictionary<TypeVariable!, Type!>! res = new Dictionary<TypeVariable!, Type!> ();
- foreach (TypeVariable! v in TypeParameters.FormalTypeParams)
+ private IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ TypeParamSubstitution() {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IDictionary<TypeVariable, Type>>()));
+ Contract.Assume(TypeParameters != null);
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ res = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
+ foreach (TypeVariable/*!*/ v in TypeParameters.FormalTypeParams) {
+ Contract.Assert(v != null);
res.Add(v, TypeParameters[v]);
+ }
return res;
}
- protected override Cmd! ComputeDesugaring() {
+ protected override Cmd ComputeDesugaring() {
+ Contract.Ensures(Contract.Result<Cmd>() != null);
CmdSeq newBlockBody = new CmdSeq();
Hashtable /*Variable -> Expr*/ substMap = new Hashtable/*Variable -> Expr*/();
Hashtable /*Variable -> Expr*/ substMapOld = new Hashtable/*Variable -> Expr*/();
Hashtable /*Variable -> Expr*/ substMapBound = new Hashtable/*Variable -> Expr*/();
- VariableSeq! tempVars = new VariableSeq();
+ VariableSeq/*!*/ tempVars = new VariableSeq();
// proc P(ins) returns (outs)
// requires Pre
- // modifies frame
+ // //modifies frame
// ensures Post
//
// call aouts := P(ains)
@@ -1579,23 +1921,22 @@ namespace Microsoft.Boogie // cframe : new variables created just for this call, to keep track of OLD values
// couts : new variables created just for this call, one per aouts
// WildcardVars : new variables created just for this call, one per null in ains
-
+
#region Create cins; each one is an incarnation of the corresponding in parameter
- VariableSeq! cins = new VariableSeq();
+ VariableSeq/*!*/ cins = new VariableSeq();
VariableSeq wildcardVars = new VariableSeq();
- assume this.Proc != null;
- for (int i = 0; i < this.Proc.InParams.Length; ++i)
- {
- Variable! param = (!)this.Proc.InParams[i];
+ Contract.Assume(this.Proc != null);
+ for (int i = 0; i < this.Proc.InParams.Length; ++i) {
+ Variable/*!*/ param = cce.NonNull(this.Proc.InParams[i]);
bool isWildcard = this.Ins[i] == null;
- Type! actualType;
+ Type/*!*/ actualType;
if (isWildcard)
actualType = param.TypedIdent.Type.Substitute(TypeParamSubstitution());
else
// during type checking, we have ensured that the type of the actual
// parameter Ins[i] is correct, so we can use it here
- actualType = (!)((!)Ins[i]).Type;
+ actualType = cce.NonNull(cce.NonNull(Ins[i]).Type);
Variable cin = CreateTemporaryVariable(tempVars, param, actualType,
TempVarKind.Formal);
@@ -1613,14 +1954,14 @@ namespace Microsoft.Boogie #endregion
#region call aouts := P(ains) becomes: (open outlining one level to see)
#region cins := ains (or havoc cin when ain is null)
- for (int i = 0, n = this.Ins.Count; i < n; i++)
- {
- IdentifierExpr! cin_exp = new IdentifierExpr(((!)cins[i]).tok, (!) cins[i]);
+ for (int i = 0, n = this.Ins.Count; i < n; i++) {
+ IdentifierExpr/*!*/ cin_exp = new IdentifierExpr(cce.NonNull(cins[i]).tok, cce.NonNull(cins[i]));
+ Contract.Assert(cin_exp != null);
if (this.Ins[i] != null) {
- AssignCmd assign = Cmd.SimpleAssign(Token.NoToken, cin_exp, (!) this.Ins[i]);
+ AssignCmd assign = Cmd.SimpleAssign(Token.NoToken, cin_exp, cce.NonNull(this.Ins[i]));
newBlockBody.Add(assign);
} else {
- IdentifierExprSeq! ies = new IdentifierExprSeq();
+ IdentifierExprSeq/*!*/ ies = new IdentifierExprSeq();
ies.Add(cin_exp);
HavocCmd havoc = new HavocCmd(Token.NoToken, ies);
newBlockBody.Add(havoc);
@@ -1632,60 +1973,62 @@ namespace Microsoft.Boogie Substitution s = Substituter.SubstitutionFromHashtable(substMapBound);
bool hasWildcard = (wildcardVars.Length != 0);
Expr preConjunction = null;
- for (int i = 0; i < this.Proc.Requires.Length; i++)
- {
- Requires! req = (!) this.Proc.Requires[i];
+ for (int i = 0; i < this.Proc.Requires.Length; i++) {
+ Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);
if (!req.Free) {
if (hasWildcard) {
- Expr pre = Substituter.Apply(s, req.Condition);
- if (preConjunction == null) {
- preConjunction = pre;
- } else {
- preConjunction = Expr.And(preConjunction, pre);
- }
+ Expr pre = Substituter.Apply(s, req.Condition);
+ if (preConjunction == null) {
+ preConjunction = pre;
+ } else {
+ preConjunction = Expr.And(preConjunction, pre);
+ }
} else {
- Requires! reqCopy = (Requires!) req.Clone();
- reqCopy.Condition = Substituter.Apply(s, req.Condition);
- AssertCmd! a = new AssertRequiresCmd(this, reqCopy);
- a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
- newBlockBody.Add(a);
+ Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());
+ reqCopy.Condition = Substituter.Apply(s, req.Condition);
+ AssertCmd/*!*/ a = new AssertRequiresCmd(this, reqCopy);
+ Contract.Assert(a != null);
+ a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
+ newBlockBody.Add(a);
}
}
}
if (hasWildcard) {
- if (preConjunction == null) {
- preConjunction = Expr.True;
- }
- Expr! expr = new ExistsExpr(tok, wildcardVars, preConjunction);
- AssertCmd! a = new AssertCmd(tok, expr);
- a.ErrorDataEnhanced = AssertCmd.GenerateBoundVarMiningStrategy(expr);
- newBlockBody.Add(a);
+ if (preConjunction == null) {
+ preConjunction = Expr.True;
+ }
+ Expr/*!*/ expr = new ExistsExpr(tok, wildcardVars, preConjunction);
+ Contract.Assert(expr != null);
+ AssertCmd/*!*/ a = new AssertCmd(tok, expr);
+ Contract.Assert(a != null);
+ a.ErrorDataEnhanced = AssertCmd.GenerateBoundVarMiningStrategy(expr);
+ newBlockBody.Add(a);
}
#endregion
#region assume Pre[ins := cins] with formal paramters
if (hasWildcard) {
- s = Substituter.SubstitutionFromHashtable(substMap);
- for (int i = 0; i < this.Proc.Requires.Length; i++)
- {
- Requires! req = (!) this.Proc.Requires[i];
- if (!req.Free) {
- Requires! reqCopy = (Requires!) req.Clone();
- reqCopy.Condition = Substituter.Apply(s, req.Condition);
- AssumeCmd! a = new AssumeCmd(tok, reqCopy.Condition);
- newBlockBody.Add(a);
- }
+ s = Substituter.SubstitutionFromHashtable(substMap);
+ for (int i = 0; i < this.Proc.Requires.Length; i++) {
+ Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);
+ if (!req.Free) {
+ Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());
+ reqCopy.Condition = Substituter.Apply(s, req.Condition);
+ AssumeCmd/*!*/ a = new AssumeCmd(tok, reqCopy.Condition);
+ Contract.Assert(a != null);
+ newBlockBody.Add(a);
}
+ }
}
#endregion
#region cframe := frame (to hold onto frame values in case they are referred to in the postcondition)
IdentifierExprSeq havocVarExprs = new IdentifierExprSeq();
- foreach (IdentifierExpr! f in this.Proc.Modifies)
- {
- assume f.Decl != null;
- assert f.Type != null;
+ foreach (IdentifierExpr/*!*/ f in this.Proc.Modifies) {
+ Contract.Assert(f != null);
+ Contract.Assume(f.Decl != null);
+ Contract.Assert(f.Type != null);
Variable v = CreateTemporaryVariable(tempVars, f.Decl, f.Type, TempVarKind.Old);
IdentifierExpr v_exp = new IdentifierExpr(v.tok, v);
substMapOld.Add(f.Decl, v_exp); // this assumes no duplicates in this.Proc.Modifies
@@ -1693,24 +2036,23 @@ namespace Microsoft.Boogie newBlockBody.Add(assign);
// fra
- if(!havocVarExprs.Has(f))
+ if (!havocVarExprs.Has(f))
havocVarExprs.Add(f);
}
#endregion
#region Create couts
- VariableSeq! couts = new VariableSeq();
- for (int i = 0; i < this.Proc.OutParams.Length; ++i)
- {
- Variable! param = (!)this.Proc.OutParams[i];
+ VariableSeq/*!*/ couts = new VariableSeq();
+ for (int i = 0; i < this.Proc.OutParams.Length; ++i) {
+ Variable/*!*/ param = cce.NonNull(this.Proc.OutParams[i]);
bool isWildcard = this.Outs[i] == null;
- Type! actualType;
+ Type/*!*/ actualType;
if (isWildcard)
actualType = param.TypedIdent.Type.Substitute(TypeParamSubstitution());
else
// during type checking, we have ensured that the type of the actual
// out parameter Outs[i] is correct, so we can use it here
- actualType = (!)((!)Outs[i]).Type;
+ actualType = cce.NonNull(cce.NonNull(Outs[i]).Type);
Variable cout = CreateTemporaryVariable(tempVars, param, actualType,
TempVarKind.Formal);
@@ -1718,15 +2060,16 @@ namespace Microsoft.Boogie IdentifierExpr ie = new IdentifierExpr(cout.tok, cout);
substMap.Add(param, ie);
- if(!havocVarExprs.Has(ie))
+ if (!havocVarExprs.Has(ie))
havocVarExprs.Add(ie);
}
// add the where clauses, now that we have the entire substitution map
- foreach (Variable! param in this.Proc.OutParams) {
+ foreach (Variable/*!*/ param in this.Proc.OutParams) {
+ Contract.Assert(param != null);
Expr w = param.TypedIdent.WhereExpr;
if (w != null) {
- IdentifierExpr ie = (IdentifierExpr!)substMap[param];
- assert ie.Decl != null;
+ IdentifierExpr ie = (IdentifierExpr/*!*/)cce.NonNull(substMap[param]);
+ Contract.Assert(ie.Decl != null);
ie.Decl.TypedIdent.WhereExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(substMap), w);
}
}
@@ -1741,8 +2084,8 @@ namespace Microsoft.Boogie #region assume Post[ins, outs, old(frame) := cins, couts, cframe]
Substitution s2 = Substituter.SubstitutionFromHashtable(substMap);
Substitution s2old = Substituter.SubstitutionFromHashtable(substMapOld);
- foreach (Ensures! e in this.Proc.Ensures)
- {
+ foreach (Ensures/*!*/ e in this.Proc.Ensures) {
+ Contract.Assert(e != null);
Expr copy = Substituter.ApplyReplacingOldExprs(s2, s2old, e.Condition);
AssumeCmd assume = new AssumeCmd(this.tok, copy);
newBlockBody.Add(assume);
@@ -1750,12 +2093,12 @@ namespace Microsoft.Boogie #endregion
#region aouts := couts
- for (int i = 0, n = this.Outs.Count; i < n; i++)
- {
- if (this.Outs[i]!=null) {
- Variable! param_i = (!) this.Proc.OutParams[i];
- Expr! cout_exp = new IdentifierExpr(((!)couts[i]).tok, (!) couts[i]);
- AssignCmd assign = Cmd.SimpleAssign(param_i.tok, (!) this.Outs[i], cout_exp);
+ for (int i = 0, n = this.Outs.Count; i < n; i++) {
+ if (this.Outs[i] != null) {
+ Variable/*!*/ param_i = cce.NonNull(this.Proc.OutParams[i]);
+ Expr/*!*/ cout_exp = new IdentifierExpr(cce.NonNull(couts[i]).tok, cce.NonNull(couts[i]));
+ Contract.Assert(cout_exp != null);
+ AssignCmd assign = Cmd.SimpleAssign(param_i.tok, cce.NonNull(this.Outs[i]), cout_exp);
newBlockBody.Add(assign);
}
}
@@ -1765,37 +2108,49 @@ namespace Microsoft.Boogie return new StateCmd(this.tok, tempVars, newBlockBody);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitCallCmd(this);
}
}
- public class CallForallCmd : CallCommonality
- {
- string! callee;
+ public class CallForallCmd : CallCommonality {
+ string/*!*/ callee;
public Procedure Proc;
- public List<Expr>! Ins;
+ public List<Expr>/*!*/ Ins;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(callee != null);
+ Contract.Invariant(Ins != null);
+ }
+
// the types of the formal in-parameters after instantiating all
// type variables whose value could be inferred using the given
// actual non-wildcard arguments
public TypeSeq InstantiatedTypes;
- public CallForallCmd(IToken! tok, string! callee, List<Expr>! ins)
- {
- base(tok, null);
+ public CallForallCmd(IToken tok, string callee, List<Expr> ins)
+ : base(tok, null) {//BASEMOVEA
+ Contract.Requires(ins != null);
+ Contract.Requires(callee != null);
+ Contract.Requires(tok != null);
+ //:base(tok, null);
this.callee = callee;
this.Ins = ins;
}
- public CallForallCmd(IToken! tok, string! callee, List<Expr>! ins, QKeyValue kv)
- {
- base(tok, kv);
+ public CallForallCmd(IToken tok, string callee, List<Expr> ins, QKeyValue kv)
+ : base(tok, kv) {//BASEMOVEA
+ Contract.Requires(ins != null);
+ Contract.Requires(callee != null);
+ Contract.Requires(tok != null);
+ //:base(tok, kv);
this.callee = callee;
this.Ins = ins;
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
stream.Write(this, level, "call ");
EmitAttributes(stream, Attributes);
stream.Write("forall ");
@@ -1814,8 +2169,8 @@ namespace Microsoft.Boogie stream.WriteLine(");");
base.Emit(stream, level);
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
if (Proc != null) {
// already resolved
return;
@@ -1831,9 +2186,11 @@ namespace Microsoft.Boogie }
}
}
- public override void AddAssignedVariables(VariableSeq! vars) { }
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void AddAssignedVariables(VariableSeq vars) {
+ //Contract.Requires(vars != null);
+ }
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
TypecheckAttributes(Attributes, tc);
// typecheck in-parameters
foreach (Expr e in Ins) {
@@ -1842,58 +2199,56 @@ namespace Microsoft.Boogie }
}
- if (this.Proc == null)
- {
+ if (this.Proc == null) {
// called procedure didn't resolve, so bug out
return;
}
// match actuals with formals
- if (Ins.Count != Proc.InParams.Length)
- {
+ if (Ins.Count != Proc.InParams.Length) {
tc.Error(this, "wrong number of in-parameters in call: {0}", callee);
- }
- else
- {
+ } else {
// determine the lists of formal and actual arguments that need
// to be matched (stars are left out)
- TypeSeq! formalTypes = new TypeSeq ();
- ExprSeq! actualArgs = new ExprSeq ();
- for (int i = 0; i < Ins.Count; i++)
+ TypeSeq/*!*/ formalTypes = new TypeSeq();
+ ExprSeq/*!*/ actualArgs = new ExprSeq();
+ for (int i = 0; i < Ins.Count; i++)
if (Ins[i] != null) {
- formalTypes.Add(((!)Proc.InParams[i]).TypedIdent.Type);
+ formalTypes.Add(cce.NonNull(Proc.InParams[i]).TypedIdent.Type);
actualArgs.Add(Ins[i]);
}
- IDictionary<TypeVariable!, Type!>! subst =
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst =
Type.MatchArgumentTypes(Proc.TypeParameters,
formalTypes, actualArgs, null, null,
"call forall to " + callee, tc);
+ Contract.Assert(cce.NonNullElements(subst));
- InstantiatedTypes = new TypeSeq ();
- foreach (Variable! var in Proc.InParams) {
+ InstantiatedTypes = new TypeSeq();
+ foreach (Variable/*!*/ var in Proc.InParams) {
+ Contract.Assert(var != null);
InstantiatedTypes.Add(var.TypedIdent.Type.Substitute(subst));
}
}
-// if (Proc.OutParams.Length != 0)
-// {
-// tc.Error(this, "call forall is allowed only on procedures with no out-parameters: {0}", callee);
-// }
+ // if (Proc.OutParams.Length != 0)
+ // {
+ // tc.Error(this, "call forall is allowed only on procedures with no out-parameters: {0}", callee);
+ // }
- if (Proc.Modifies.Length != 0)
- {
+ if (Proc.Modifies.Length != 0) {
tc.Error(this, "call forall is allowed only on procedures with no modifies clause: {0}", callee);
}
}
- protected override Cmd! ComputeDesugaring() {
+ protected override Cmd ComputeDesugaring() {
+ Contract.Ensures(Contract.Result<Cmd>() != null);
CmdSeq newBlockBody = new CmdSeq();
Hashtable /*Variable -> Expr*/ substMap = new Hashtable/*Variable -> Expr*/();
- VariableSeq! tempVars = new VariableSeq();
+ VariableSeq/*!*/ tempVars = new VariableSeq();
// proc P(ins) returns ()
// requires Pre;
- // modifies ;
+ // //modifies ;
// ensures Post;
//
// call forall P(ains);
@@ -1904,12 +2259,12 @@ namespace Microsoft.Boogie // wildcardVars : the bound variables to be wrapped up in a quantification
#region Create cins; each one is an incarnation of the corresponding in parameter
- VariableSeq! cins = new VariableSeq();
+ VariableSeq cins = new VariableSeq();
VariableSeq wildcardVars = new VariableSeq();
- assume this.Proc != null;
+ Contract.Assume(this.Proc != null);
for (int i = 0, n = this.Proc.InParams.Length; i < n; i++) {
- Variable param = (!)this.Proc.InParams[i];
- Type! paramType = ((!)this.InstantiatedTypes)[i]; // might contain type variables
+ Variable param = cce.NonNull(this.Proc.InParams[i]);
+ Type/*!*/ paramType = cce.NonNull(this.InstantiatedTypes)[i]; // might contain type variables
bool isWildcard = this.Ins[i] == null;
Variable cin = CreateTemporaryVariable(tempVars, param, paramType,
isWildcard ? TempVarKind.Bound : TempVarKind.Formal);
@@ -1926,11 +2281,10 @@ namespace Microsoft.Boogie #region call forall P(ains) becomes: (open outlining one level to see)
#region cins := ains
- for (int i = 0, n = this.Ins.Count; i < n; i++)
- {
+ for (int i = 0, n = this.Ins.Count; i < n; i++) {
if (this.Ins[i] != null) {
- IdentifierExpr! cin_exp = new IdentifierExpr(((!)cins[i]).tok, (!) cins[i]);
- AssignCmd assign = Cmd.SimpleAssign(Token.NoToken, cin_exp, (!) this.Ins[i]);
+ IdentifierExpr/*!*/ cin_exp = new IdentifierExpr(cce.NonNull(cins[i]).tok, cce.NonNull(cins[i]));
+ AssignCmd assign = Cmd.SimpleAssign(Token.NoToken, cin_exp, cce.NonNull(this.Ins[i]));
newBlockBody.Add(assign);
}
}
@@ -1939,9 +2293,8 @@ namespace Microsoft.Boogie #region assert Pre[ins := cins]
Substitution s = Substituter.SubstitutionFromHashtable(substMap);
Expr preConjunction = null;
- for (int i = 0; i < this.Proc.Requires.Length; i++)
- {
- Requires! req = (!) this.Proc.Requires[i];
+ for (int i = 0; i < this.Proc.Requires.Length; i++) {
+ Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);
if (!req.Free) {
Expr pre = Substituter.Apply(s, req.Condition);
if (preConjunction == null) {
@@ -1957,9 +2310,9 @@ namespace Microsoft.Boogie #endregion
#region Create couts
- VariableSeq! couts = new VariableSeq();
- foreach ( Variable! param in this.Proc.OutParams )
- {
+ VariableSeq/*!*/ couts = new VariableSeq();
+ foreach (Variable/*!*/ param in this.Proc.OutParams) {
+ Contract.Assert(param != null);
Variable cout = CreateTemporaryVariable(tempVars, param,
param.TypedIdent.Type, TempVarKind.Bound);
couts.Add(cout);
@@ -1967,11 +2320,12 @@ namespace Microsoft.Boogie substMap.Add(param, ie);
}
// add the where clauses, now that we have the entire substitution map
- foreach (Variable! param in this.Proc.OutParams) {
+ foreach (Variable/*!*/ param in this.Proc.OutParams) {
+ Contract.Assert(param != null);
Expr w = param.TypedIdent.WhereExpr;
if (w != null) {
- IdentifierExpr ie = (IdentifierExpr!)substMap[param];
- assert ie.Decl != null;
+ IdentifierExpr ie = (IdentifierExpr)cce.NonNull(substMap[param]);
+ Contract.Assert(ie.Decl != null);
ie.Decl.TypedIdent.WhereExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(substMap), w);
}
}
@@ -1980,8 +2334,8 @@ namespace Microsoft.Boogie #region assume Post[ins := cins]
s = Substituter.SubstitutionFromHashtable(substMap);
Expr postConjunction = null;
- foreach (Ensures! e in this.Proc.Ensures)
- {
+ foreach (Ensures/*!*/ e in this.Proc.Ensures) {
+ Contract.Assert(e != null);
Expr post = Substituter.Apply(s, e.Condition);
if (postConjunction == null) {
postConjunction = post;
@@ -1997,11 +2351,11 @@ namespace Microsoft.Boogie #region assume (forall wildcardVars :: Pre ==> Post);
Expr body = postConjunction;
if (couts.Length > 0) {
- body = new ExistsExpr(tok, couts, body);
+ body = new ExistsExpr(tok, couts, body);
}
body = Expr.Imp(preConjunction, body);
if (wildcardVars.Length != 0) {
- TypeVariableSeq! typeParams = Type.FreeVariablesIn((!)InstantiatedTypes);
+ TypeVariableSeq/*!*/ typeParams = Type.FreeVariablesIn(cce.NonNull(InstantiatedTypes));
body = new ForallExpr(tok, typeParams, wildcardVars, body);
}
newBlockBody.Add(new AssumeCmd(tok, body));
@@ -2011,25 +2365,33 @@ namespace Microsoft.Boogie return new StateCmd(this.tok, tempVars, newBlockBody);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitCallForallCmd(this);
}
}
- public abstract class PredicateCmd : Cmd
- {
- public /*readonly--except in StandardVisitor*/ Expr! Expr;
- public PredicateCmd(IToken! tok, Expr! expr)
- : base(tok)
- {
+ public abstract class PredicateCmd : Cmd {
+ public /*readonly--except in StandardVisitor*/ Expr/*!*/ Expr;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Expr != null);
+ }
+
+ public PredicateCmd(IToken/*!*/ tok, Expr/*!*/ expr)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(expr != null);
Expr = expr;
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
Expr.Resolve(rc);
}
- public override void AddAssignedVariables(VariableSeq! vars) { }
+ public override void AddAssignedVariables(VariableSeq vars) {
+ //Contract.Requires(vars != null);
+ }
}
public abstract class MiningStrategy {
@@ -2038,33 +2400,50 @@ namespace Microsoft.Boogie }
public class ListOfMiningStrategies : MiningStrategy {
- public List<MiningStrategy>! msList;
+ public List<MiningStrategy>/*!*/ msList;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(msList != null);
+ }
- public ListOfMiningStrategies (List<MiningStrategy>! l) {
+
+ public ListOfMiningStrategies(List<MiningStrategy> l) {
+ Contract.Requires(l != null);
this.msList = l;
}
}
public class EEDTemplate : MiningStrategy {
- public string! reason;
- public List<Expr!>! exprList;
+ public string/*!*/ reason;
+ public List<Expr/*!*/>/*!*/ exprList;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(reason != null);
+ Contract.Invariant(cce.NonNullElements(exprList));
+ }
- public EEDTemplate (string! reason, List<Expr!>! exprList) {
+
+ public EEDTemplate(string reason, List<Expr/*!*/>/*!*/ exprList) {
+ Contract.Requires(reason != null);
+ Contract.Requires(cce.NonNullElements(exprList));
this.reason = reason;
this.exprList = exprList;
}
}
- public class AssertCmd : PredicateCmd, IPotentialErrorNode
- {
+ public class AssertCmd : PredicateCmd, IPotentialErrorNode {
public Expr OrigExpr;
public Hashtable /*Variable -> Expr*/ IncarnationMap;
// TODO: convert to use generics
private object errorData;
public object ErrorData {
- get { return errorData; }
- set { errorData = value; }
+ get {
+ return errorData;
+ }
+ set {
+ errorData = value;
+ }
}
public string ErrorMessage {
@@ -2077,48 +2456,54 @@ namespace Microsoft.Boogie private MiningStrategy errorDataEnhanced;
public MiningStrategy ErrorDataEnhanced {
- get { return errorDataEnhanced; }
- set { errorDataEnhanced = value; }
+ get {
+ return errorDataEnhanced;
+ }
+ set {
+ errorDataEnhanced = value;
+ }
}
- public AssertCmd(IToken! tok, Expr! expr)
- : base(tok, expr)
- {
+ public AssertCmd(IToken/*!*/ tok, Expr/*!*/ expr)
+ : base(tok, expr) {
+ Contract.Requires(tok != null);
+ Contract.Requires(expr != null);
errorDataEnhanced = GenerateBoundVarMiningStrategy(expr);
}
- public AssertCmd(IToken! tok, Expr! expr, QKeyValue kv)
- : base(tok, expr)
- {
+ public AssertCmd(IToken/*!*/ tok, Expr/*!*/ expr, QKeyValue kv)
+ : base(tok, expr) {
+ Contract.Requires(tok != null);
+ Contract.Requires(expr != null);
errorDataEnhanced = GenerateBoundVarMiningStrategy(expr);
Attributes = kv;
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
stream.Write(this, level, "assert ");
EmitAttributes(stream, Attributes);
this.Expr.Emit(stream);
stream.WriteLine(";");
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
ResolveAttributes(Attributes, rc);
base.Resolve(rc);
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
TypecheckAttributes(Attributes, tc);
Expr.Typecheck(tc);
- assert Expr.Type != null; // follows from Expr.Typecheck postcondition
- if (!Expr.Type.Unify(Type.Bool))
- {
+ Contract.Assert(Expr.Type != null); // follows from Expr.Typecheck postcondition
+ if (!Expr.Type.Unify(Type.Bool)) {
tc.Error(this, "an asserted expression must be of type bool (got: {0})", Expr.Type);
}
}
- public static MiningStrategy GenerateBoundVarMiningStrategy (Expr! expr) {
+ public static MiningStrategy GenerateBoundVarMiningStrategy(Expr expr) {
+ Contract.Requires(expr != null);
List<MiningStrategy> l = new List<MiningStrategy>();
if (expr != null) {
l = GenerateBoundVarListForMining(expr, l);
@@ -2126,29 +2511,32 @@ namespace Microsoft.Boogie return new ListOfMiningStrategies(l);
}
- public static List<MiningStrategy>! GenerateBoundVarListForMining (Expr! expr, List<MiningStrategy>! l) {
+ public static List<MiningStrategy>/*!*/ GenerateBoundVarListForMining(Expr expr, List<MiningStrategy> l) {
+ Contract.Requires(l != null);
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<List<MiningStrategy>>() != null);
+
// go through the origExpr and identify all bound variables in the AST.
if (expr is LiteralExpr || expr is IdentifierExpr) {
//end recursion
- }
- else if (expr is NAryExpr) {
+ } else if (expr is NAryExpr) {
NAryExpr e = (NAryExpr)expr;
- foreach (Expr! arg in e.Args) {
+ foreach (Expr/*!*/ arg in e.Args) {
+ Contract.Assert(arg != null);
l = GenerateBoundVarListForMining(arg, l);
}
- }
- else if (expr is OldExpr) {
+ } else if (expr is OldExpr) {
OldExpr e = (OldExpr)expr;
l = GenerateBoundVarListForMining(e.Expr, l);
- }
- else if (expr is QuantifierExpr) {
- QuantifierExpr qe = (QuantifierExpr) expr;
+ } else if (expr is QuantifierExpr) {
+ QuantifierExpr qe = (QuantifierExpr)expr;
VariableSeq vs = qe.Dummies;
- foreach (Variable! x in vs) {
+ foreach (Variable/*!*/ x in vs) {
+ Contract.Assert(x != null);
string name = x.Name;
if (name.StartsWith("^")) {
name = name.Substring(1);
- List<Expr!> exprList = new List<Expr!>();
+ List<Expr> exprList = new List<Expr>();
exprList.Add(new IdentifierExpr(Token.NoToken, x.ToString(), x.TypedIdent.Type));
MiningStrategy eed = new EEDTemplate("The bound variable " + name + " has the value {0}.", exprList);
l.Add(eed);
@@ -2160,48 +2548,56 @@ namespace Microsoft.Boogie }
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitAssertCmd(this);
}
}
// An AssertCmd that is a loop invariant check before the loop iteration starts
- public class LoopInitAssertCmd : AssertCmd
- {
- public LoopInitAssertCmd(IToken! tok, Expr! expr)
- : base(tok, expr)
- {
+ public class LoopInitAssertCmd : AssertCmd {
+ public LoopInitAssertCmd(IToken/*!*/ tok, Expr/*!*/ expr)
+ : base(tok, expr) {
+ Contract.Requires(tok != null);
+ Contract.Requires(expr != null);
}
}
// An AssertCmd that is a loop invariant check to maintain the invariant after iteration
- public class LoopInvMaintainedAssertCmd : AssertCmd
- {
- public LoopInvMaintainedAssertCmd(IToken! tok, Expr! expr)
- : base(tok, expr)
- {
+ public class LoopInvMaintainedAssertCmd : AssertCmd {
+ public LoopInvMaintainedAssertCmd(IToken/*!*/ tok, Expr/*!*/ expr)
+ : base(tok, expr) {
+ Contract.Requires(tok != null);
+ Contract.Requires(expr != null);
}
}
/// <summary>
/// An AssertCmd that is introduced in translation from the requires on a call.
/// </summary>
- public class AssertRequiresCmd : AssertCmd
- {
- public CallCmd! Call;
- public Requires! Requires;
+ public class AssertRequiresCmd : AssertCmd {
+ public CallCmd/*!*/ Call;
+ public Requires/*!*/ Requires;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Call != null);
+ Contract.Invariant(Requires != null);
+ }
- public AssertRequiresCmd(CallCmd! call, Requires! @requires)
- : base(call.tok, @requires.Condition)
- {
+
+ public AssertRequiresCmd(CallCmd/*!*/ call, Requires/*!*/ requires)
+ : base(call.tok, requires.Condition) {
+ Contract.Requires(call != null);
+ Contract.Requires(requires != null);
this.Call = call;
- this.Requires = @requires;
+ this.Requires = requires;
// base(call.tok, @requires.Condition);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitAssertRequiresCmd(this);
}
}
@@ -2210,263 +2606,284 @@ namespace Microsoft.Boogie /// An AssertCmd that is introduced in translation from an ensures
/// declaration.
/// </summary>
- public class AssertEnsuresCmd : AssertCmd
- {
- public Ensures! Ensures;
- public AssertEnsuresCmd(Ensures! ens)
- : base(ens.tok, ens.Condition)
- {
+ public class AssertEnsuresCmd : AssertCmd {
+ public Ensures/*!*/ Ensures;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Ensures != null);
+ }
+
+ public AssertEnsuresCmd(Ensures/*!*/ ens)
+ : base(ens.tok, ens.Condition) {
+ Contract.Requires(ens != null);
this.Ensures = ens;
// base(ens.tok, ens.Condition);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitAssertEnsuresCmd(this);
}
}
- public class AssumeCmd : PredicateCmd
- {
- public AssumeCmd(IToken! tok, Expr! expr)
- : base(tok, expr)
- {
- //Debug.Assert(expr != null);
+ public class AssumeCmd : PredicateCmd {
+ public AssumeCmd(IToken/*!*/ tok, Expr/*!*/ expr)
+ : base(tok, expr) {
+ Contract.Requires(tok != null);
+ Contract.Requires(expr != null);
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
stream.Write(this, level, "assume ");
this.Expr.Emit(stream);
stream.WriteLine(";");
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
Expr.Typecheck(tc);
- assert Expr.Type != null; // follows from Expr.Typecheck postcondition
- if (!Expr.Type.Unify(Type.Bool))
- {
+ 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)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitAssumeCmd(this);
}
}
- public class ReturnExprCmd : ReturnCmd
- {
- public Expr! Expr;
- public ReturnExprCmd(IToken! tok, Expr! expr)
- : base(tok)
- {
+ public class ReturnExprCmd : ReturnCmd {
+ public Expr/*!*/ Expr;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Expr != null);
+ }
+
+ public ReturnExprCmd(IToken/*!*/ tok, Expr/*!*/ expr)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(expr != null);
Expr = expr;
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
stream.Write(this, level, "return ");
this.Expr.Emit(stream);
stream.WriteLine(";");
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
Expr.Typecheck(tc);
- assert Expr.Type != null; // follows from Expr.Typecheck postcondition
- if (!Expr.Type.Unify(Type.Bool))
- {
+ Contract.Assert(Expr.Type != null); // follows from Expr.Typecheck postcondition
+ if (!Expr.Type.Unify(Type.Bool)) {
tc.Error(this, "a return expression must be of type bool (got: {0})", Expr.Type);
}
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
Expr.Resolve(rc);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitReturnExprCmd(this);
}
}
- public class HavocCmd : Cmd
- {
- public IdentifierExprSeq! Vars;
- public HavocCmd(IToken! tok, IdentifierExprSeq! vars)
- : base(tok)
- {
+ public class HavocCmd : Cmd {
+ public IdentifierExprSeq/*!*/ Vars;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Vars != null);
+ }
+
+ public HavocCmd(IToken/*!*/ tok, IdentifierExprSeq/*!*/ vars)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(vars != null);
Vars = vars;
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
stream.Write(this, level, "havoc ");
Vars.Emit(stream, true);
stream.WriteLine(";");
}
- public override void Resolve(ResolutionContext! rc)
- {
- foreach (IdentifierExpr! ide in Vars)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ foreach (IdentifierExpr/*!*/ ide in Vars) {
+ Contract.Assert(ide != null);
ide.Resolve(rc);
}
}
- public override void AddAssignedVariables(VariableSeq! vars)
- {
- foreach (IdentifierExpr! e in this.Vars)
- {
+ public override void AddAssignedVariables(VariableSeq vars) {
+ //Contract.Requires(vars != null);
+ foreach (IdentifierExpr/*!*/ e in this.Vars) {
+ Contract.Assert(e != null);
vars.Add(e.Decl);
}
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
this.CheckAssignments(tc);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitHavocCmd(this);
}
}
//---------------------------------------------------------------------
// Transfer commands
+ [ContractClass(typeof(TransferCmdContracts))]
+ public abstract class TransferCmd : Absy {
+ internal TransferCmd(IToken/*!*/ tok)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ }
+ public abstract void Emit(TokenTextWriter/*!*/ stream, int level);
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ // nothing to typecheck
+ }
+ }
+ [ContractClassFor(typeof(TransferCmd))]
+ public abstract class TransferCmdContracts : TransferCmd {
+ public TransferCmdContracts() :base(null){
- public abstract class TransferCmd : Absy
- {
- internal TransferCmd(IToken! tok)
- : base(tok)
- {
}
- public abstract void Emit(TokenTextWriter! stream, int level);
- public override void Typecheck(TypecheckingContext! tc)
- {
- // nothing to typecheck
+ public override void Emit(TokenTextWriter stream, int level) {
+ Contract.Requires(stream != null);
+ throw new NotImplementedException();
}
}
- public class ReturnCmd : TransferCmd
- {
- public ReturnCmd(IToken! tok)
- : base(tok)
- {
+ public class ReturnCmd : TransferCmd {
+ public ReturnCmd(IToken/*!*/ tok)
+ : base(tok) {
+ Contract.Requires(tok != null);
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
stream.WriteLine(this, level, "return;");
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
// nothing to resolve
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitReturnCmd(this);
}
}
- public class GotoCmd : TransferCmd
- {
+ public class GotoCmd : TransferCmd {
[Rep]
public StringSeq labelNames;
[Rep]
public BlockSeq labelTargets;
- invariant labelNames != null && labelTargets != null ==> labelNames.Length == labelTargets.Length;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(labelNames == null || labelTargets == null || labelNames.Length == labelTargets.Length);
+ }
[NotDelayed]
- public GotoCmd(IToken! tok, StringSeq! labelSeq)
- : base (tok)
- {
+ public GotoCmd(IToken/*!*/ tok, StringSeq/*!*/ labelSeq)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(labelSeq != null);
this.labelNames = labelSeq;
}
- public GotoCmd(IToken! tok, StringSeq! labelSeq, BlockSeq! blockSeq)
- : base (tok)
- {
+ public GotoCmd(IToken/*!*/ tok, StringSeq/*!*/ labelSeq, BlockSeq/*!*/ blockSeq)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(labelSeq != null);
+ Contract.Requires(blockSeq != null);
Debug.Assert(labelSeq.Length == blockSeq.Length);
- for (int i=0; i<labelSeq.Length; i++) { Debug.Assert(Equals(labelSeq[i], ((!)blockSeq[i]).Label)); }
+ for (int i = 0; i < labelSeq.Length; i++) {
+ Debug.Assert(Equals(labelSeq[i], cce.NonNull(blockSeq[i]).Label));
+ }
this.labelNames = labelSeq;
this.labelTargets = blockSeq;
}
- public GotoCmd(IToken! tok, BlockSeq! blockSeq)
- : base (tok)
- { //requires blockSeq[i] != null ==> blockSeq[i].Label != null;
+ public GotoCmd(IToken/*!*/ tok, BlockSeq/*!*/ blockSeq)
+ : base(tok) { //requires (blockSeq[i] != null ==> blockSeq[i].Label != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(blockSeq != null);
StringSeq labelSeq = new StringSeq();
- for (int i=0; i<blockSeq.Length; i++)
- labelSeq.Add(((!)blockSeq[i]).Label);
+ for (int i = 0; i < blockSeq.Length; i++)
+ labelSeq.Add(cce.NonNull(blockSeq[i]).Label);
this.labelNames = labelSeq;
this.labelTargets = blockSeq;
}
- public void AddTarget(Block! b)
- requires b.Label != null;
- requires this.labelTargets != null;
- requires this.labelNames != null;
- {
+ public void AddTarget(Block b) {
+ Contract.Requires(b != null);
+ Contract.Requires(b.Label != null);
+ Contract.Requires(this.labelTargets != null);
+ Contract.Requires(this.labelNames != null);
this.labelTargets.Add(b);
this.labelNames.Add(b.Label);
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
- assume this.labelNames != null;
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
+ Contract.Assume(this.labelNames != null);
stream.Write(this, level, "goto ");
- if (CommandLineOptions.Clo.PrintWithUniqueASTIds)
- {
- if (labelTargets == null)
- {
+ if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
+ if (labelTargets == null) {
string sep = "";
- foreach (string name in labelNames)
- {
+ foreach (string name in labelNames) {
stream.Write("{0}{1}^^{2}", sep, "NoDecl", name);
sep = ", ";
}
- }
- else
- {
+ } else {
string sep = "";
- foreach (Block! b in labelTargets)
- {
+ foreach (Block/*!*/ b in labelTargets) {
+ Contract.Assert(b != null);
stream.Write("{0}h{1}^^{2}", sep, b.GetHashCode(), b.Label);
sep = ", ";
}
}
- }
- else
- {
+ } else {
labelNames.Emit(stream);
}
stream.WriteLine(";");
}
- public override void Resolve(ResolutionContext! rc)
- ensures labelTargets != null;
- {
- if (labelTargets != null)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ Contract.Ensures(labelTargets != null);
+ if (labelTargets != null) {
// already resolved
return;
}
- assume this.labelNames != null;
+ Contract.Assume(this.labelNames != null);
labelTargets = new BlockSeq();
- foreach (string! lbl in labelNames)
- {
+ foreach (string/*!*/ lbl in labelNames) {
+ Contract.Assert(lbl != null);
Block b = rc.LookUpBlock(lbl);
- if (b == null)
- {
+ if (b == null) {
rc.Error(this, "goto to unknown block: {0}", lbl);
- }
- else
- {
+ } else {
labelTargets.Add(b);
}
}
Debug.Assert(rc.ErrorCount > 0 || labelTargets.Length == labelNames.Length);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitGotoCmd(this);
}
}
-
-}
+}
\ No newline at end of file |