diff options
| author |  tabarbe <unknown> | 2010-08-20 22:32:24 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-20 22:32:24 +0000 |
| commit | 72b39a6962d7f6c7ca1aab9919791238c7baba3f (patch) | |
| tree | 75bb9c1b956d1b368f4cf2983a20a913211dd350 /Source/Core/Absy.cs | |
| parent | 96d9624e9e22dbe9090e0bd7d538cafbf0a16463 (diff) | |
Boogie: Committing changed source files
Diffstat (limited to 'Source/Core/Absy.cs')
| -rw-r--r-- | Source/Core/Absy.cs | 3273 |
1 files changed, 1768 insertions, 1505 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 4d0113ee..e8fdc385 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -6,23 +6,33 @@ //---------------------------------------------------------------------------------------------
// BoogiePL - Absy.cs
//---------------------------------------------------------------------------------------------
-namespace Microsoft.Boogie.AbstractInterpretation
-{
+namespace Microsoft.Boogie.AbstractInterpretation {
using System.Diagnostics;
+ using System.Diagnostics.Contracts;
using CCI = System.Compiler;
using System.Collections;
using AI = Microsoft.AbstractInterpretationFramework;
- public class CallSite
- {
- public readonly Implementation! Impl;
- public readonly Block! Block;
+ public class CallSite {
+ public readonly Implementation/*!*/ Impl;
+ public readonly Block/*!*/ Block;
public readonly int Statement; // invariant: Block[Statement] is CallCmd
- public readonly AI.Lattice.Element! KnownBeforeCall;
- public readonly ProcedureSummaryEntry! SummaryEntry;
-
- public CallSite (Implementation! impl, Block! b, int stmt, AI.Lattice.Element! e, ProcedureSummaryEntry! summaryEntry)
- {
+ public readonly AI.Lattice.Element/*!*/ KnownBeforeCall;
+ public readonly ProcedureSummaryEntry/*!*/ SummaryEntry;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Impl != null);
+ Contract.Invariant(Block != null);
+ Contract.Invariant(KnownBeforeCall != null);
+ Contract.Invariant(SummaryEntry != null);
+ }
+
+
+ public CallSite(Implementation impl, Block b, int stmt, AI.Lattice.Element e, ProcedureSummaryEntry summaryEntry) {
+ Contract.Requires(summaryEntry != null);
+ Contract.Requires(e != null);
+ Contract.Requires(b != null);
+ Contract.Requires(impl != null);
this.Impl = impl;
this.Block = b;
this.Statement = stmt;
@@ -31,15 +41,23 @@ namespace Microsoft.Boogie.AbstractInterpretation }
}
- public class ProcedureSummaryEntry
- {
- public AI.Lattice! Lattice;
- public AI.Lattice.Element! OnEntry;
- public AI.Lattice.Element! OnExit;
- public CCI.IMutableSet/*<CallSite>*/! ReturnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints
+ public class ProcedureSummaryEntry {
+ public AI.Lattice/*!*/ Lattice;
+ public AI.Lattice.Element/*!*/ OnEntry;
+ public AI.Lattice.Element/*!*/ OnExit;
+ public CCI.IMutableSet/*<CallSite>*//*!*/ ReturnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Lattice != null);
+ Contract.Invariant(OnEntry != null);
+ Contract.Invariant(OnExit != null);
+ Contract.Invariant(ReturnPoints != null);
+ }
- public ProcedureSummaryEntry (AI.Lattice! lattice, AI.Lattice.Element! onEntry)
- {
+
+ public ProcedureSummaryEntry(AI.Lattice lattice, AI.Lattice.Element onEntry) {
+ Contract.Requires(onEntry != null);
+ Contract.Requires(lattice != null);
this.Lattice = lattice;
this.OnEntry = onEntry;
this.OnExit = lattice.Bottom;
@@ -51,41 +69,56 @@ namespace Microsoft.Boogie.AbstractInterpretation public class ProcedureSummary : ArrayList/*<ProcedureSummaryEntry>*/
{
- invariant !IsReadOnly && !IsFixedSize;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(
+ !IsReadOnly && !IsFixedSize);
+ }
- public new ProcedureSummaryEntry! this [int i]
- {
- get
- requires 0 <= i && i < Count;
- { return (ProcedureSummaryEntry!) base[i]; }
+ public new ProcedureSummaryEntry/*!*/ this[int i] {
+ get {
+ Contract.Requires(0 <= i && i < Count);
+ Contract.Ensures(Contract.Result<ProcedureSummaryEntry>() != null);
+ return cce.NonNull((ProcedureSummaryEntry/*!*/)base[i]);
+ }
}
} // class
} // namespace
-
-namespace Microsoft.Boogie
-{
+namespace Microsoft.Boogie {
using System;
using System.Collections;
using System.Diagnostics;
using System.Collections.Generic;
+ using System.Diagnostics.Contracts;
using Microsoft.Boogie.AbstractInterpretation;
using AI = Microsoft.AbstractInterpretationFramework;
- using Microsoft.Contracts;
using Graphing;
-
- public abstract class Absy
- {
- public IToken! tok;
+ [ContractClass(typeof(AbsyContracts))]
+ public abstract class Absy {
+ public IToken/*!*/ tok;
private int uniqueId;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(tok != null);
+ }
+
- public int Line { get { return tok != null ? tok.line : -1; } }
- public int Col { get { return tok != null ? tok.col : -1; } }
+ public int Line {
+ get {
+ return tok != null ? tok.line : -1;
+ }
+ }
+ public int Col {
+ get {
+ return tok != null ? tok.col : -1;
+ }
+ }
- public Absy (IToken! tok)
- {
+ public Absy(IToken tok) {
+ Contract.Requires(tok != null);
this.tok = tok;
this.uniqueId = AbsyNodeCount++;
// base();
@@ -96,59 +129,85 @@ namespace Microsoft.Boogie // We uniquely number every AST node to make them
// suitable for our implementation of functional maps.
//
- public int UniqueId { get { return this.uniqueId; } }
+ public int UniqueId {
+ get {
+ return this.uniqueId;
+ }
+ }
private const int indent_size = 2;
- protected static string Indent (int level)
- {
+ protected static string Indent(int level) {
return new string(' ', (indent_size * level));
}
-
- public abstract void Resolve (ResolutionContext! rc);
+ [NeedsContracts]
+ public abstract void Resolve(ResolutionContext/*!*/ rc);
/// <summary>
/// Requires the object to have been successfully resolved.
/// </summary>
/// <param name="tc"></param>
- public abstract void Typecheck (TypecheckingContext! tc);
+ [NeedsContracts]
+ public abstract void Typecheck(TypecheckingContext/*!*/ tc);
/// <summary>
/// Intorduced this so the uniqueId is not the same on a cloned object.
/// </summary>
/// <param name="tc"></param>
- public virtual Absy! Clone()
- {
- Absy! result = (Absy!) this.MemberwiseClone();
+ public virtual Absy Clone() {
+ Contract.Ensures(Contract.Result<Absy>() != null);
+ Absy/*!*/ result = cce.NonNull((Absy/*!*/)this.MemberwiseClone());
result.uniqueId = AbsyNodeCount++; // BUGBUG??
return result;
}
- public virtual Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public virtual Absy StdDispatch(StandardVisitor visitor) {
+ Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
System.Diagnostics.Debug.Fail("Unknown Absy node type: " + this.GetType());
throw new System.NotImplementedException();
}
}
+ [ContractClassFor(typeof(Absy))]
+ public abstract class AbsyContracts : Absy {
+ public override void Resolve(ResolutionContext rc) {
+ Contract.Requires(rc != null);
+ throw new NotImplementedException();
+ }
+ public AbsyContracts() :base(null){
+
+ }
+ public override void Typecheck(TypecheckingContext tc) {
+ Contract.Requires(tc != null);
+ throw new NotImplementedException();
+ }
+ }
+
// TODO: Ideally, this would use generics.
- public interface IPotentialErrorNode
- {
- object ErrorData { get; set; }
+ public interface IPotentialErrorNode {
+ object ErrorData {
+ get;
+ set;
+ }
}
- public class Program : Absy
- {
+ public class Program : Absy {
[Rep]
- public List<Declaration!>! TopLevelDeclarations;
+ public List<Declaration/*!*/>/*!*/ TopLevelDeclarations;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(TopLevelDeclarations));
+ Contract.Invariant(globals == null || cce.NonNullElements(globals));
+ }
+
public Program()
- : base(Token.NoToken)
- {
- this.TopLevelDeclarations = new List<Declaration!>();
+ : base(Token.NoToken) {
+ this.TopLevelDeclarations = new List<Declaration>();
// base(Token.NoToken);
}
- public void Emit (TokenTextWriter! stream)
- {
+ public void Emit(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
stream.SetToken(this);
Emitter.Declarations(this.TopLevelDeclarations, stream);
}
@@ -156,29 +215,27 @@ namespace Microsoft.Boogie /// Returns the number of name resolution errors.
/// </summary>
/// <returns></returns>
- public int Resolve ()
- {
- return Resolve((IErrorSink) null);
+ public int Resolve() {
+ return Resolve((IErrorSink)null);
}
- public int Resolve (IErrorSink errorSink)
- {
+ public int Resolve(IErrorSink errorSink) {
ResolutionContext rc = new ResolutionContext(errorSink);
Resolve(rc);
return rc.ErrorCount;
}
- public override void Resolve (ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
Helpers.ExtraTraceInformation("Starting resolution");
-
+
foreach (Declaration d in TopLevelDeclarations) {
d.Register(rc);
}
ResolveTypes(rc);
- List<Declaration!> prunedTopLevelDecls = CommandLineOptions.Clo.OverlookBoogieTypeErrors ? new List<Declaration!>() : null;
+ List<Declaration/*!*/> prunedTopLevelDecls = CommandLineOptions.Clo.OverlookBoogieTypeErrors ? new List<Declaration/*!*/>() : null;
foreach (Declaration d in TopLevelDeclarations) {
// resolve all the non-type-declarations
@@ -212,7 +269,8 @@ namespace Microsoft.Boogie }
- private void ResolveTypes (ResolutionContext! rc) {
+ private void ResolveTypes(ResolutionContext rc) {
+ Contract.Requires(rc != null);
// first resolve type constructors
foreach (Declaration d in TopLevelDeclarations) {
if (d is TypeCtorDecl)
@@ -220,8 +278,9 @@ namespace Microsoft.Boogie }
// collect type synonym declarations
- List<TypeSynonymDecl!>! synonymDecls = new List<TypeSynonymDecl!> ();
+ List<TypeSynonymDecl/*!*/>/*!*/ synonymDecls = new List<TypeSynonymDecl/*!*/>();
foreach (Declaration d in TopLevelDeclarations) {
+ Contract.Assert(d != null);
if (d is TypeSynonymDecl)
synonymDecls.Add((TypeSynonymDecl)d);
}
@@ -230,22 +289,19 @@ namespace Microsoft.Boogie // fixed-point iteration
TypeSynonymDecl.ResolveTypeSynonyms(synonymDecls, rc);
}
-
- public int Typecheck ()
- {
- return this.Typecheck((IErrorSink) null);
+ public int Typecheck() {
+ return this.Typecheck((IErrorSink)null);
}
- public int Typecheck (IErrorSink errorSink)
- {
+ public int Typecheck(IErrorSink errorSink) {
TypecheckingContext tc = new TypecheckingContext(errorSink);
Typecheck(tc);
return tc.ErrorCount;
}
- public override void Typecheck (TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
Helpers.ExtraTraceInformation("Starting typechecking");
int oldErrorCount = tc.ErrorCount;
@@ -255,7 +311,7 @@ namespace Microsoft.Boogie if (oldErrorCount == tc.ErrorCount) {
// check whether any type proxies have remained uninstantiated
- TypeAmbiguitySeeker! seeker = new TypeAmbiguitySeeker (tc);
+ TypeAmbiguitySeeker/*!*/ seeker = new TypeAmbiguitySeeker(tc);
foreach (Declaration d in TopLevelDeclarations) {
seeker.Visit(d);
}
@@ -265,15 +321,13 @@ namespace Microsoft.Boogie expander.CollectExpansions();
}
- public void ComputeStronglyConnectedComponents()
- {
- foreach(Declaration d in this.TopLevelDeclarations) {
+ public void ComputeStronglyConnectedComponents() {
+ foreach (Declaration d in this.TopLevelDeclarations) {
d.ComputeStronglyConnectedComponents();
}
}
- public void InstrumentWithInvariants ()
- {
+ public void InstrumentWithInvariants() {
foreach (Declaration d in this.TopLevelDeclarations) {
d.InstrumentWithInvariants();
}
@@ -282,301 +336,300 @@ namespace Microsoft.Boogie /// <summary>
/// Reset the abstract stated computed before
/// </summary>
- public void ResetAbstractInterpretationState()
- {
- foreach(Declaration d in this.TopLevelDeclarations) {
+ public void ResetAbstractInterpretationState() {
+ foreach (Declaration d in this.TopLevelDeclarations) {
d.ResetAbstractInterpretationState();
}
}
- public void UnrollLoops(int n)
- requires 0 <= n;
- {
+ public void UnrollLoops(int n) {
+ Contract.Requires(0 <= n);
foreach (Declaration d in this.TopLevelDeclarations) {
Implementation impl = d as Implementation;
if (impl != null && impl.Blocks != null && impl.Blocks.Count > 0) {
- expose (impl) {
+ cce.BeginExpose(impl);
+ {
Block start = impl.Blocks[0];
- assume start != null;
- assume start.IsConsistent;
+ Contract.Assume(start != null);
+ Contract.Assume(cce.IsConsistent(start));
impl.Blocks = LoopUnroll.UnrollLoops(start, n);
}
+ cce.EndExpose();
}
}
}
- void CreateProceduresForLoops(Implementation! impl, Graph<Block!>! g, List<Implementation!>! loopImpls)
- {
- // Enumerate the headers
- // for each header h:
- // create implementation p_h with
- // inputs = inputs, outputs, and locals of impl
- // outputs = outputs and locals of impl
- // locals = empty set
- // add call o := p_h(i) at the beginning of the header block
- // break the back edges whose target is h
- // Enumerate the headers again to create the bodies of p_h
- // for each header h:
- // compute the loop corresponding to h
- // make copies of all blocks in the loop for h
- // delete all target edges that do not go to a block in the loop
- // create a new entry block and a new return block
- // add edges from entry block to the loop header and the return block
- // add calls o := p_h(i) at the end of the blocks that are sources of back edges
- Dictionary<Block!, string!>! loopHeaderToName = new Dictionary<Block!, string!>();
- Dictionary<Block!, VariableSeq!>! loopHeaderToInputs = new Dictionary<Block!, VariableSeq!>();
- Dictionary<Block!, VariableSeq!>! loopHeaderToOutputs = new Dictionary<Block!, VariableSeq!>();
- Dictionary<Block!, Hashtable!>! loopHeaderToSubstMap = new Dictionary<Block!, Hashtable!>();
- Dictionary<Block!, Procedure!>! loopHeaderToLoopProc = new Dictionary<Block!, Procedure!>();
- Dictionary<Block!, CallCmd!>! loopHeaderToCallCmd = new Dictionary<Block!, CallCmd!>();
- foreach (Block! header in g.Headers)
- {
- Contract.Assert(header != null);
- string name = header.ToString();
- loopHeaderToName[header] = name;
- VariableSeq inputs = new VariableSeq();
- VariableSeq outputs = new VariableSeq();
- ExprSeq callInputs = new ExprSeq();
- IdentifierExprSeq callOutputs = new IdentifierExprSeq();
- Hashtable substMap = new Hashtable(); // Variable -> IdentifierExpr
-
- foreach (Variable! v in impl.InParams)
- {
- callInputs.Add(new IdentifierExpr(Token.NoToken, v));
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in_" + v.Name, v.TypedIdent.Type), true);
- inputs.Add(f);
- substMap[v] = new IdentifierExpr(Token.NoToken, f);
- }
- foreach (Variable! v in impl.OutParams)
- {
- callInputs.Add(new IdentifierExpr(Token.NoToken, v));
- inputs.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in_" + v.Name, v.TypedIdent.Type), true));
- callOutputs.Add(new IdentifierExpr(Token.NoToken, v));
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out_" + v.Name, v.TypedIdent.Type), false);
- outputs.Add(f);
- substMap[v] = new IdentifierExpr(Token.NoToken, f);
- }
- foreach (Variable! v in impl.LocVars)
- {
- callInputs.Add(new IdentifierExpr(Token.NoToken, v));
- inputs.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in_" + v.Name, v.TypedIdent.Type), true));
- callOutputs.Add(new IdentifierExpr(Token.NoToken, v));
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out_" + v.Name, v.TypedIdent.Type), false);
- outputs.Add(f);
- substMap[v] = new IdentifierExpr(Token.NoToken, f);
+ void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g, List<Implementation/*!*/>/*!*/ loopImpls) {
+ Contract.Requires(impl != null);
+ Contract.Requires(cce.NonNullElements(loopImpls));
+ Contract.Requires(cce.NonNullElements(g.TopologicalSort()));
+ // Enumerate the headers
+ // for each header h:
+ // create implementation p_h with
+ // inputs = inputs, outputs, and locals of impl
+ // outputs = outputs and locals of impl
+ // locals = empty set
+ // add call o := p_h(i) at the beginning of the header block
+ // break the back edges whose target is h
+ // Enumerate the headers again to create the bodies of p_h
+ // for each header h:
+ // compute the loop corresponding to h
+ // make copies of all blocks in the loop for h
+ // delete all target edges that do not go to a block in the loop
+ // create a new entry block and a new return block
+ // add edges from entry block to the loop header and the return block
+ // add calls o := p_h(i) at the end of the blocks that are sources of back edges
+ Dictionary<Block/*!*/, string/*!*/>/*!*/ loopHeaderToName = new Dictionary<Block/*!*/, string/*!*/>();
+ Dictionary<Block/*!*/, VariableSeq/*!*/>/*!*/ loopHeaderToInputs = new Dictionary<Block/*!*/, VariableSeq/*!*/>();
+ Dictionary<Block/*!*/, VariableSeq/*!*/>/*!*/ loopHeaderToOutputs = new Dictionary<Block/*!*/, VariableSeq/*!*/>();
+ Dictionary<Block/*!*/, Hashtable/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary<Block/*!*/, Hashtable/*!*/>();
+ Dictionary<Block/*!*/, Procedure/*!*/>/*!*/ loopHeaderToLoopProc = new Dictionary<Block/*!*/, Procedure/*!*/>();
+ Dictionary<Block/*!*/, CallCmd/*!*/>/*!*/ loopHeaderToCallCmd = new Dictionary<Block/*!*/, CallCmd/*!*/>();
+ foreach (Block/*!*/ header in g.Headers) {
+ Contract.Assert(header != null);
+ Contract.Assert(header != null);
+ string name = header.ToString();
+ loopHeaderToName[header] = name;
+ VariableSeq inputs = new VariableSeq();
+ VariableSeq outputs = new VariableSeq();
+ ExprSeq callInputs = new ExprSeq();
+ IdentifierExprSeq callOutputs = new IdentifierExprSeq();
+ Hashtable substMap = new Hashtable(); // Variable -> IdentifierExpr
+
+ foreach (Variable/*!*/ v in impl.InParams) {
+ Contract.Assert(v != null);
+ callInputs.Add(new IdentifierExpr(Token.NoToken, v));
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in_" + v.Name, v.TypedIdent.Type), true);
+ inputs.Add(f);
+ substMap[v] = new IdentifierExpr(Token.NoToken, f);
+ }
+ foreach (Variable/*!*/ v in impl.OutParams) {
+ Contract.Assert(v != null);
+ callInputs.Add(new IdentifierExpr(Token.NoToken, v));
+ inputs.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in_" + v.Name, v.TypedIdent.Type), true));
+ callOutputs.Add(new IdentifierExpr(Token.NoToken, v));
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out_" + v.Name, v.TypedIdent.Type), false);
+ outputs.Add(f);
+ substMap[v] = new IdentifierExpr(Token.NoToken, f);
+ }
+ foreach (Variable/*!*/ v in impl.LocVars) {
+ Contract.Assert(v != null);
+ callInputs.Add(new IdentifierExpr(Token.NoToken, v));
+ inputs.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in_" + v.Name, v.TypedIdent.Type), true));
+ callOutputs.Add(new IdentifierExpr(Token.NoToken, v));
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out_" + v.Name, v.TypedIdent.Type), false);
+ outputs.Add(f);
+ substMap[v] = new IdentifierExpr(Token.NoToken, f);
+ }
+ VariableSeq/*!*/ targets = new VariableSeq();
+ foreach (Block/*!*/ b in g.BackEdgeNodes(header)) {
+ Contract.Assert(b != null);
+ foreach (Block/*!*/ block in g.NaturalLoops(header, b)) {
+ Contract.Assert(block != null);
+ foreach (Cmd/*!*/ cmd in block.Cmds) {
+ Contract.Assert(cmd != null);
+ cmd.AddAssignedVariables(targets);
}
- VariableSeq! targets = new VariableSeq();
- foreach (Block! b in g.BackEdgeNodes(header))
- {
- foreach (Block! block in g.NaturalLoops(header, b))
- {
- foreach (Cmd! cmd in block.Cmds)
- {
- cmd.AddAssignedVariables(targets);
- }
+ }
+ }
+ IdentifierExprSeq/*!*/ globalMods = new IdentifierExprSeq();
+ Set globalModsSet = new Set();
+ foreach (Variable/*!*/ v in targets) {
+ Contract.Assert(v != null);
+ if (!(v is GlobalVariable))
+ continue;
+ if (globalModsSet.Contains(v))
+ continue;
+ globalModsSet.Add(v);
+ globalMods.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ loopHeaderToInputs[header] = inputs;
+ loopHeaderToOutputs[header] = outputs;
+ loopHeaderToSubstMap[header] = substMap;
+ Procedure/*!*/ proc =
+ new Procedure(Token.NoToken, "loop_" + header.ToString(),
+ new TypeVariableSeq(), inputs, outputs,
+ new RequiresSeq(), globalMods, new EnsuresSeq());
+ if (CommandLineOptions.Clo.LazyInlining > 0 || CommandLineOptions.Clo.StratifiedInlining > 0) {
+ proc.AddAttribute("inline", Expr.Literal(1));
+ }
+ loopHeaderToLoopProc[header] = proc;
+ CallCmd callCmd = new CallCmd(Token.NoToken, name, callInputs, callOutputs);
+ callCmd.Proc = proc;
+ loopHeaderToCallCmd[header] = callCmd;
+ }
+
+ foreach (Block/*!*/ header in g.Headers) {
+ Contract.Assert(header != null);
+ Procedure loopProc = loopHeaderToLoopProc[header];
+ Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
+ CodeCopier codeCopier = new CodeCopier(loopHeaderToSubstMap[header]); // fix me
+ VariableSeq inputs = loopHeaderToInputs[header];
+ VariableSeq outputs = loopHeaderToOutputs[header];
+ foreach (Block/*!*/ source in g.BackEdgeNodes(header)) {
+ Contract.Assert(source != null);
+ foreach (Block/*!*/ block in g.NaturalLoops(header, source)) {
+ Contract.Assert(block != null);
+ if (blockMap.ContainsKey(block))
+ continue;
+ Block newBlock = new Block();
+ newBlock.Label = block.Label;
+ newBlock.Cmds = codeCopier.CopyCmdSeq(block.Cmds);
+ blockMap[block] = newBlock;
+ }
+ string callee = loopHeaderToName[header];
+ ExprSeq ins = new ExprSeq();
+ IdentifierExprSeq outs = new IdentifierExprSeq();
+ for (int i = 0; i < impl.InParams.Length; i++) {
+ ins.Add(new IdentifierExpr(Token.NoToken, cce.NonNull(inputs[i])));
+ }
+ foreach (Variable/*!*/ v in outputs) {
+ Contract.Assert(v != null);
+ ins.Add(new IdentifierExpr(Token.NoToken, v));
+ outs.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ CallCmd callCmd = new CallCmd(Token.NoToken, callee, ins, outs);
+ callCmd.Proc = loopProc;
+ Block/*!*/ block1 = new Block(Token.NoToken, source.Label + "_dummy",
+ new CmdSeq(new AssumeCmd(Token.NoToken, Expr.False)), new ReturnCmd(Token.NoToken));
+ Block/*!*/ block2 = new Block(Token.NoToken, block1.Label,
+ new CmdSeq(callCmd), new ReturnCmd(Token.NoToken));
+ impl.Blocks.Add(block1);
+
+ GotoCmd gotoCmd = source.TransferCmd as GotoCmd;
+ Contract.Assert(gotoCmd != null && gotoCmd.labelNames != null && gotoCmd.labelTargets != null && gotoCmd.labelTargets.Length >= 1);
+ StringSeq/*!*/ newLabels = new StringSeq();
+ BlockSeq/*!*/ newTargets = new BlockSeq();
+ for (int i = 0; i < gotoCmd.labelTargets.Length; i++) {
+ if (gotoCmd.labelTargets[i] == header)
+ continue;
+ newTargets.Add(gotoCmd.labelTargets[i]);
+ newLabels.Add(gotoCmd.labelNames[i]);
+ }
+ newTargets.Add(block1);
+ newLabels.Add(block1.Label);
+ gotoCmd.labelNames = newLabels;
+ gotoCmd.labelTargets = newTargets;
+
+ blockMap[block1] = block2;
+ }
+ List<Block/*!*/>/*!*/ blocks = new List<Block/*!*/>();
+ Block exit = new Block(Token.NoToken, "exit", new CmdSeq(), new ReturnCmd(Token.NoToken));
+ GotoCmd cmd = new GotoCmd(Token.NoToken,
+ new StringSeq(cce.NonNull(blockMap[header]).Label, exit.Label),
+ new BlockSeq(blockMap[header], exit));
+
+ Debug.Assert(outputs.Length + impl.InParams.Length == inputs.Length);
+ List<AssignLhs/*!*/>/*!*/ lhss = new List<AssignLhs/*!*/>();
+ List<Expr/*!*/>/*!*/ rhss = new List<Expr/*!*/>();
+ for (int i = impl.InParams.Length; i < inputs.Length; i++) {
+ Variable/*!*/ inv = cce.NonNull(inputs[i]);
+ Variable/*!*/ outv = cce.NonNull(outputs[i - impl.InParams.Length]);
+ AssignLhs lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, outv));
+ Expr rhs = new IdentifierExpr(Token.NoToken, inv);
+ lhss.Add(lhs);
+ rhss.Add(rhs);
+ }
+ AssignCmd assignCmd = new AssignCmd(Token.NoToken, lhss, rhss);
+ Block entry = new Block(Token.NoToken, "entry", new CmdSeq(assignCmd), cmd);
+ blocks.Add(entry);
+ foreach (Block/*!*/ block in blockMap.Keys) {
+ Contract.Assert(block != null);
+ Block/*!*/ newBlock = cce.NonNull(blockMap[block]);
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ if (gotoCmd == null) {
+ newBlock.TransferCmd = new ReturnCmd(Token.NoToken);
+ } else {
+ Contract.Assume(gotoCmd.labelNames != null && gotoCmd.labelTargets != null);
+ StringSeq newLabels = new StringSeq();
+ BlockSeq newTargets = new BlockSeq();
+ for (int i = 0; i < gotoCmd.labelTargets.Length; i++) {
+ Block target = gotoCmd.labelTargets[i];
+ if (blockMap.ContainsKey(target)) {
+ newLabels.Add(gotoCmd.labelNames[i]);
+ newTargets.Add(blockMap[target]);
}
}
- IdentifierExprSeq! globalMods = new IdentifierExprSeq();
- Set globalModsSet = new Set();
- foreach (Variable! v in targets)
- {
- if (!(v is GlobalVariable)) continue;
- if (globalModsSet.Contains(v)) continue;
- globalModsSet.Add(v);
- globalMods.Add(new IdentifierExpr(Token.NoToken, v));
- }
- loopHeaderToInputs[header] = inputs;
- loopHeaderToOutputs[header] = outputs;
- loopHeaderToSubstMap[header] = substMap;
- Procedure! proc =
- new Procedure(Token.NoToken, "loop_" + header.ToString(),
- new TypeVariableSeq(), inputs, outputs,
- new RequiresSeq(), globalMods, new EnsuresSeq());
- if (CommandLineOptions.Clo.LazyInlining > 0 || CommandLineOptions.Clo.StratifiedInlining > 0)
- {
- proc.AddAttribute("inline", Expr.Literal(1));
+ if (newTargets.Length == 0) {
+ newBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
+ newBlock.TransferCmd = new ReturnCmd(Token.NoToken);
+ } else {
+ newBlock.TransferCmd = new GotoCmd(Token.NoToken, newLabels, newTargets);
}
- loopHeaderToLoopProc[header] = proc;
- CallCmd callCmd = new CallCmd(Token.NoToken, name, callInputs, callOutputs);
- callCmd.Proc = proc;
- loopHeaderToCallCmd[header] = callCmd;
+ }
+ blocks.Add(newBlock);
}
+ blocks.Add(exit);
+ Implementation loopImpl =
+ new Implementation(Token.NoToken, loopProc.Name,
+ new TypeVariableSeq(), inputs, outputs, new VariableSeq(), blocks);
+ loopImpl.Proc = loopProc;
+ loopImpls.Add(loopImpl);
- foreach (Block! header in g.Headers)
- {
- Procedure loopProc = loopHeaderToLoopProc[header];
- Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
- CodeCopier codeCopier = new CodeCopier(loopHeaderToSubstMap[header]); // fix me
- VariableSeq inputs = loopHeaderToInputs[header];
- VariableSeq outputs = loopHeaderToOutputs[header];
- foreach (Block! source in g.BackEdgeNodes(header))
- {
- foreach (Block! block in g.NaturalLoops(header, source))
- {
- if (blockMap.ContainsKey(block)) continue;
- Block newBlock = new Block();
- newBlock.Label = block.Label;
- newBlock.Cmds = codeCopier.CopyCmdSeq(block.Cmds);
- blockMap[block] = newBlock;
- }
- string callee = loopHeaderToName[header];
- ExprSeq ins = new ExprSeq();
- IdentifierExprSeq outs = new IdentifierExprSeq();
- for (int i = 0; i < impl.InParams.Length; i++)
- {
- ins.Add(new IdentifierExpr(Token.NoToken, (!) inputs[i]));
- }
- foreach (Variable! v in outputs)
- {
- ins.Add(new IdentifierExpr(Token.NoToken, v));
- outs.Add(new IdentifierExpr(Token.NoToken, v));
- }
- CallCmd callCmd = new CallCmd(Token.NoToken, callee, ins, outs);
- callCmd.Proc = loopProc;
- Block! block1 = new Block(Token.NoToken, source.Label + "_dummy",
- new CmdSeq(new AssumeCmd(Token.NoToken, Expr.False)), new ReturnCmd(Token.NoToken));
- Block! block2 = new Block(Token.NoToken, block1.Label,
- new CmdSeq(callCmd), new ReturnCmd(Token.NoToken));
- impl.Blocks.Add(block1);
-
- GotoCmd gotoCmd = source.TransferCmd as GotoCmd;
- assert gotoCmd != null && gotoCmd.labelNames != null && gotoCmd.labelTargets != null && gotoCmd.labelTargets.Length >= 1;
- StringSeq! newLabels = new StringSeq();
- BlockSeq! newTargets = new BlockSeq();
- for (int i = 0; i < gotoCmd.labelTargets.Length; i++)
- {
- if (gotoCmd.labelTargets[i] == header) continue;
- newTargets.Add(gotoCmd.labelTargets[i]);
- newLabels.Add(gotoCmd.labelNames[i]);
- }
- newTargets.Add(block1);
- newLabels.Add(block1.Label);
- gotoCmd.labelNames = newLabels;
- gotoCmd.labelTargets = newTargets;
-
- blockMap[block1] = block2;
- }
- List<Block!>! blocks = new List<Block!>();
- Block exit = new Block(Token.NoToken, "exit", new CmdSeq(), new ReturnCmd(Token.NoToken));
- GotoCmd cmd = new GotoCmd(Token.NoToken,
- new StringSeq(((!)blockMap[header]).Label, exit.Label),
- new BlockSeq(blockMap[header], exit));
-
- Debug.Assert(outputs.Length + impl.InParams.Length == inputs.Length);
- List<AssignLhs!>! lhss = new List<AssignLhs!>();
- List<Expr!>! rhss = new List<Expr!>();
- for (int i = impl.InParams.Length; i < inputs.Length; i++)
- {
- Variable! inv = (!)inputs[i];
- Variable! outv = (!)outputs[i - impl.InParams.Length];
- AssignLhs lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, outv));
- Expr rhs = new IdentifierExpr(Token.NoToken, inv);
- lhss.Add(lhs);
- rhss.Add(rhs);
- }
- AssignCmd assignCmd = new AssignCmd(Token.NoToken, lhss, rhss);
- Block entry = new Block(Token.NoToken, "entry", new CmdSeq(assignCmd), cmd);
- blocks.Add(entry);
- foreach (Block! block in blockMap.Keys)
- {
- Block! newBlock = (!) blockMap[block];
- GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
- if (gotoCmd == null)
- {
- newBlock.TransferCmd = new ReturnCmd(Token.NoToken);
- }
- else
- {
- assume gotoCmd.labelNames != null && gotoCmd.labelTargets != null;
- StringSeq newLabels = new StringSeq();
- BlockSeq newTargets = new BlockSeq();
- for (int i = 0; i < gotoCmd.labelTargets.Length; i++)
- {
- Block target = gotoCmd.labelTargets[i];
- if (blockMap.ContainsKey(target))
- {
- newLabels.Add(gotoCmd.labelNames[i]);
- newTargets.Add(blockMap[target]);
- }
- }
- if (newTargets.Length == 0)
- {
- newBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
- newBlock.TransferCmd = new ReturnCmd(Token.NoToken);
- }
- else
- {
- newBlock.TransferCmd = new GotoCmd(Token.NoToken, newLabels, newTargets);
- }
- }
- blocks.Add(newBlock);
- }
- blocks.Add(exit);
- Implementation loopImpl =
- new Implementation(Token.NoToken, loopProc.Name,
- new TypeVariableSeq(), inputs, outputs, new VariableSeq(), blocks);
- loopImpl.Proc = loopProc;
- loopImpls.Add(loopImpl);
-
- // Finally, add call to the loop in the containing procedure
- CmdSeq cmdSeq = new CmdSeq();
- cmdSeq.Add(loopHeaderToCallCmd[header]);
- cmdSeq.AddRange(header.Cmds);
- header.Cmds = cmdSeq;
- }
- }
-
- public static Graph<Block!>! GraphFromImpl(Implementation! impl) {
+ // Finally, add call to the loop in the containing procedure
+ CmdSeq cmdSeq = new CmdSeq();
+ cmdSeq.Add(loopHeaderToCallCmd[header]);
+ cmdSeq.AddRange(header.Cmds);
+ header.Cmds = cmdSeq;
+ }
+ }
+
+ public static Graph<Block/*!*/>/*!*/ GraphFromImpl(Implementation impl) {
+ Contract.Requires(impl != null);
+ Contract.Ensures(cce.NonNullElements(Contract.Result<Graph<Block>>().TopologicalSort()));
Contract.Ensures(Contract.Result<Graph<Block>>() != null);
- Graph<Block!> g = new Graph<Block!>();
+ Graph<Block/*!*/> g = new Graph<Block/*!*/>();
g.AddSource(impl.Blocks[0]); // there is always at least one node in the graph
foreach (Block b in impl.Blocks) {
Contract.Assert(b != null);
GotoCmd gtc = b.TransferCmd as GotoCmd;
if (gtc != null) {
- foreach (Block! dest in (!)gtc.labelTargets) {
+ foreach (Block/*!*/ dest in cce.NonNull(gtc.labelTargets)) {
+ Contract.Assert(dest != null);
g.AddEdge(b, dest);
}
}
}
return g;
}
-
- public void ExtractLoops()
- {
- List<Implementation!>! loopImpls = new List<Implementation!>();
+
+ public void ExtractLoops() {
+ List<Implementation/*!*/>/*!*/ loopImpls = new List<Implementation/*!*/>();
foreach (Declaration d in this.TopLevelDeclarations) {
Implementation impl = d as Implementation;
if (impl != null && impl.Blocks != null && impl.Blocks.Count > 0) {
- Graph<Block!>! g = GraphFromImpl(impl);
- g.ComputeLoops();
- if (!g.Reducible)
- {
- throw new Exception("Irreducible flow graphs are unsupported.");
- }
- CreateProceduresForLoops(impl, g, loopImpls);
+ Graph<Block/*!*/>/*!*/ g = GraphFromImpl(impl);
+ Contract.Assert(cce.NonNullElements(g.TopologicalSort()));
+ g.ComputeLoops();
+ if (!g.Reducible) {
+ throw new Exception("Irreducible flow graphs are unsupported.");
+ }
+ CreateProceduresForLoops(impl, g, loopImpls);
}
}
- foreach (Implementation! loopImpl in loopImpls)
- {
+ foreach (Implementation/*!*/ loopImpl in loopImpls) {
+ Contract.Assert(loopImpl != null);
TopLevelDeclarations.Add(loopImpl);
}
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitProgram(this);
}
-
- private List<GlobalVariable!> globals = null;
- public List<GlobalVariable!>! GlobalVariables()
- {
- if (globals != null) return globals;
- globals = new List<GlobalVariable!>();
+
+ private List<GlobalVariable/*!*/> globals = null;
+ public List<GlobalVariable/*!*/>/*!*/ GlobalVariables() {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<GlobalVariable>>()));
+ if (globals != null)
+ return globals;
+ globals = new List<GlobalVariable/*!*/>();
foreach (Declaration d in TopLevelDeclarations) {
GlobalVariable gvar = d as GlobalVariable;
- if (gvar != null) globals.Add(gvar);
+ if (gvar != null)
+ globals.Add(gvar);
}
return globals;
}
@@ -585,32 +638,32 @@ namespace Microsoft.Boogie //---------------------------------------------------------------------
// Declarations
- public abstract class Declaration : Absy
- {
+ [ContractClass(typeof(DeclarationContracts))]
+ public abstract class Declaration : Absy {
public QKeyValue Attributes;
- public Declaration(IToken! tok)
- : base(tok)
- {
+ public Declaration(IToken tok)
+ : base(tok) {
+ Contract.Requires(tok != null);
}
- protected void EmitAttributes(TokenTextWriter! stream)
- {
+ protected void EmitAttributes(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
kv.Emit(stream);
stream.Write(" ");
}
}
- protected void ResolveAttributes(ResolutionContext! rc)
- {
+ protected void ResolveAttributes(ResolutionContext rc) {
+ Contract.Requires(rc != null);
for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
kv.Resolve(rc);
}
}
- protected void TypecheckAttributes(TypecheckingContext! rc)
- {
+ protected void TypecheckAttributes(TypecheckingContext rc) {
+ Contract.Requires(rc != null);
for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
kv.Typecheck(rc);
}
@@ -620,9 +673,9 @@ namespace Microsoft.Boogie // (which is not touched if there is no attribute specified).
//
// Returns false is there was an error processing the flag, true otherwise.
- public bool CheckBooleanAttribute(string! name, ref bool result)
- {
- Expr? expr = FindExprAttribute(name);
+ public bool CheckBooleanAttribute(string name, ref bool result) {
+ Contract.Requires(name != null);
+ Expr expr = FindExprAttribute(name);
if (expr != null) {
if (expr is LiteralExpr && ((LiteralExpr)expr).isBool) {
result = ((LiteralExpr)expr).asBool;
@@ -634,9 +687,9 @@ namespace Microsoft.Boogie }
// Look for {:name expr} in list of attributes.
- public Expr? FindExprAttribute(string! name)
- {
- Expr? res = null;
+ public Expr FindExprAttribute(string name) {
+ Contract.Requires(name != null);
+ Expr res = null;
for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
if (kv.Key == name) {
if (kv.Params.Count == 1 && kv.Params[0] is Expr) {
@@ -648,8 +701,8 @@ namespace Microsoft.Boogie }
// Look for {:name string} in list of attributes.
- public string? FindStringAttribute(string! name)
- {
+ public string FindStringAttribute(string name) {
+ Contract.Requires(name != null);
return QKeyValue.FindStringAttribute(this.Attributes, name);
}
@@ -657,9 +710,9 @@ namespace Microsoft.Boogie // (which is not touched if there is no attribute specified).
//
// Returns false is there was an error processing the flag, true otherwise.
- public bool CheckIntAttribute(string! name, ref int result)
- {
- Expr? expr = FindExprAttribute(name);
+ public bool CheckIntAttribute(string name, ref int result) {
+ Contract.Requires(name != null);
+ Expr expr = FindExprAttribute(name);
if (expr != null) {
if (expr is LiteralExpr && ((LiteralExpr)expr).isBigNum) {
result = ((LiteralExpr)expr).asBigNum.ToInt;
@@ -670,8 +723,9 @@ namespace Microsoft.Boogie return true;
}
- public void AddAttribute(string! name, object! val)
- {
+ public void AddAttribute(string name, object val) {
+ Contract.Requires(val != null);
+ Contract.Requires(name != null);
QKeyValue kv;
for (kv = this.Attributes; kv != null; kv = kv.Next) {
if (kv.Key == name) {
@@ -680,58 +734,83 @@ namespace Microsoft.Boogie }
}
if (kv == null) {
- Attributes = new QKeyValue(tok, name, new List<object!>(new object![] { val }), Attributes);
+ Attributes = new QKeyValue(tok, name, new List<object/*!*/>(new object/*!*/[] { val }), Attributes);
}
- }
-
- public abstract void Emit(TokenTextWriter! stream, int level);
- public abstract void Register(ResolutionContext! rc);
+ }
+
+ public abstract void Emit(TokenTextWriter/*!*/ stream, int level);
+ public abstract void Register(ResolutionContext/*!*/ rc);
/// <summary>
/// Compute the strongly connected components of the declaration.
/// By default, it does nothing
/// </summary>
- public virtual void ComputeStronglyConnectedComponents() { /* Does nothing */}
+ public virtual void ComputeStronglyConnectedComponents() { /* Does nothing */
+ }
/// <summary>
/// This method inserts the abstract-interpretation-inferred invariants
/// as assume (or possibly assert) statements in the statement sequences of
/// each block.
/// </summary>
- public virtual void InstrumentWithInvariants () {}
+ public virtual void InstrumentWithInvariants() {
+ }
/// <summary>
/// Reset the abstract stated computed before
/// </summary>
- public virtual void ResetAbstractInterpretationState() { /* does nothing */ }
+ public virtual void ResetAbstractInterpretationState() { /* does nothing */
+ }
+ }
+ [ContractClassFor(typeof(Declaration))]
+ public abstract class DeclarationContracts : Declaration {
+ public DeclarationContracts() :base(null){
+ }
+ public override void Register(ResolutionContext rc) {
+ Contract.Requires(rc != null);
+ throw new NotImplementedException();
+ }
+ public override void Emit(TokenTextWriter stream, int level) {
+ Contract.Requires(stream != null);
+ throw new NotImplementedException();
+ }
}
- public class Axiom : Declaration
- {
- public Expr! Expr;
- public string? Comment;
+ public class Axiom : Declaration {
+ public Expr/*!*/ Expr;
+ [ContractInvariantMethod]
+ void ExprInvariant() {
+ Contract.Invariant(Expr != null);
+ }
- public Axiom(IToken! tok, Expr! expr)
- {
- this(tok, expr, null);
+ public string Comment;
+
+ public Axiom(IToken tok, Expr expr)
+ : this(tok, expr, null) {
+ Contract.Requires(expr != null);
+ Contract.Requires(tok != null);
+ //:this(tok, expr, null);//BASEMOVEA
}
- public Axiom(IToken! tok, Expr! expr, string? comment)
- : base(tok)
- {
+ public Axiom(IToken/*!*/ tok, Expr/*!*/ expr, string comment)
+ : base(tok) {//BASEMOVE DANGER
+ Contract.Requires(tok != null);
+ Contract.Requires(expr != null);
Expr = expr;
Comment = comment;
- // base(tok);
+ // :base(tok);
}
- public Axiom(IToken! tok, Expr! expr, string? comment, QKeyValue kv)
- {
- this(tok, expr, comment);
+ public Axiom(IToken tok, Expr expr, string comment, QKeyValue kv)
+ : this(tok, expr, comment) {//BASEMOVEA
+ Contract.Requires(expr != null);
+ Contract.Requires(tok != null);
+ //:this(tok, expr, comment);
this.Attributes = kv;
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
if (Comment != null) {
stream.WriteLine(this, level, "// " + Comment);
}
@@ -740,80 +819,86 @@ namespace Microsoft.Boogie this.Expr.Emit(stream);
stream.WriteLine(";");
}
- public override void Register(ResolutionContext! rc)
- {
+ public override void Register(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
// nothing to register
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
ResolveAttributes(rc);
rc.StateMode = ResolutionContext.State.StateLess;
Expr.Resolve(rc);
rc.StateMode = ResolutionContext.State.Single;
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
TypecheckAttributes(tc);
Expr.Typecheck(tc);
- assert Expr.Type != null; // follows from postcondition of Expr.Typecheck
- if (! Expr.Type.Unify(Type.Bool))
- {
+ Contract.Assert(Expr.Type != null); // follows from postcondition of Expr.Typecheck
+ if (!Expr.Type.Unify(Type.Bool)) {
tc.Error(this, "axioms must be of type bool");
}
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitAxiom(this);
}
}
- public abstract class NamedDeclaration : Declaration
- {
- private string! name;
- public string! Name
- {
- get
- {
+ public abstract class NamedDeclaration : Declaration {
+ private string/*!*/ name;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(name != null);
+ }
+
+ public string/*!*/ Name {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
+
return this.name;
}
- set
- {
+ set {
+ Contract.Requires(value != null);
this.name = value;
}
}
- public NamedDeclaration(IToken! tok, string! name)
- : base(tok)
- {
+ public NamedDeclaration(IToken/*!*/ tok, string/*!*/ name)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
this.name = name;
// base(tok);
}
[Pure]
- public override string! ToString()
- {
- return (!) Name;
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return cce.NonNull(Name);
}
- }
+ }
- public class TypeCtorDecl : NamedDeclaration
- {
+ public class TypeCtorDecl : NamedDeclaration {
public readonly int Arity;
- public TypeCtorDecl(IToken! tok, string! name, int Arity)
- : base(tok, name)
- {
- this.Arity = Arity;
- }
- public TypeCtorDecl(IToken! tok, string! name, int Arity, QKeyValue kv)
- : base(tok, name)
- {
- this.Arity = Arity;
- this.Attributes = kv;
+ public TypeCtorDecl(IToken/*!*/ tok, string/*!*/ name, int Arity)
+ : base(tok, name) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ this.Arity = Arity;
+ }
+ public TypeCtorDecl(IToken/*!*/ tok, string/*!*/ name, int Arity, QKeyValue kv)
+ : base(tok, name) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ this.Arity = Arity;
+ this.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, "type ");
EmitAttributes(stream);
stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(Name));
@@ -821,48 +906,59 @@ namespace Microsoft.Boogie stream.Write(" _");
stream.WriteLine(";");
}
- public override void Register(ResolutionContext! rc)
- {
+ public override void Register(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
rc.AddType(this);
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
ResolveAttributes(rc);
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
TypecheckAttributes(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.VisitTypeCtorDecl(this);
}
}
+ public class TypeSynonymDecl : NamedDeclaration {
+ public TypeVariableSeq/*!*/ TypeParameters;
+ public Type/*!*/ Body;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(TypeParameters != null);
+ Contract.Invariant(Body != null);
+ }
- public class TypeSynonymDecl : NamedDeclaration
- {
- public TypeVariableSeq! TypeParameters;
- public Type! Body;
- public TypeSynonymDecl(IToken! tok, string! name,
- TypeVariableSeq! typeParams, Type! body)
- : base(tok, name)
- {
+ public TypeSynonymDecl(IToken/*!*/ tok, string/*!*/ name,
+ TypeVariableSeq/*!*/ typeParams, Type/*!*/ body)
+ : base(tok, name) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(body != null);
this.TypeParameters = typeParams;
this.Body = body;
}
- public TypeSynonymDecl(IToken! tok, string! name,
- TypeVariableSeq! typeParams, Type! body, QKeyValue kv)
- : base(tok, name)
- {
+ public TypeSynonymDecl(IToken/*!*/ tok, string/*!*/ name,
+ TypeVariableSeq/*!*/ typeParams, Type/*!*/ body, QKeyValue kv)
+ : base(tok, name) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(body != null);
this.TypeParameters = typeParams;
this.Body = body;
this.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, "type ");
EmitAttributes(stream);
stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(Name));
@@ -873,46 +969,51 @@ namespace Microsoft.Boogie Body.Emit(stream);
stream.WriteLine(";");
}
- public override void Register(ResolutionContext! rc)
- {
+ public override void Register(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
rc.AddType(this);
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
ResolveAttributes(rc);
int previousState = rc.TypeBinderState;
try {
- foreach (TypeVariable! v in TypeParameters)
+ foreach (TypeVariable/*!*/ v in TypeParameters) {
+ Contract.Assert(v != null);
rc.AddTypeBinder(v);
+ }
Body = Body.ResolveType(rc);
} finally {
rc.TypeBinderState = previousState;
}
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
TypecheckAttributes(tc);
}
- public static void ResolveTypeSynonyms(List<TypeSynonymDecl!>! synonymDecls,
- ResolutionContext! rc) {
+ public static void ResolveTypeSynonyms(List<TypeSynonymDecl/*!*/>/*!*/ synonymDecls, ResolutionContext/*!*/ rc) {
+ Contract.Requires(cce.NonNullElements(synonymDecls));
+ Contract.Requires(rc != null);
// then discover all dependencies between type synonyms
- IDictionary<TypeSynonymDecl!, List<TypeSynonymDecl!>!>! deps =
- new Dictionary<TypeSynonymDecl!, List<TypeSynonymDecl!>!> ();
- foreach (TypeSynonymDecl! decl in synonymDecls) {
- List<TypeSynonymDecl!>! declDeps = new List<TypeSynonymDecl!> ();
+ IDictionary<TypeSynonymDecl/*!*/, List<TypeSynonymDecl/*!*/>/*!*/>/*!*/ deps =
+ new Dictionary<TypeSynonymDecl/*!*/, List<TypeSynonymDecl/*!*/>/*!*/>();
+ foreach (TypeSynonymDecl/*!*/ decl in synonymDecls) {
+ Contract.Assert(decl != null);
+ List<TypeSynonymDecl/*!*/>/*!*/ declDeps = new List<TypeSynonymDecl/*!*/>();
FindDependencies(decl.Body, declDeps, rc);
deps.Add(decl, declDeps);
}
- List<TypeSynonymDecl!>! resolved = new List<TypeSynonymDecl!> ();
+ List<TypeSynonymDecl/*!*/>/*!*/ resolved = new List<TypeSynonymDecl/*!*/>();
int unresolved = synonymDecls.Count - resolved.Count;
while (unresolved > 0) {
- foreach (TypeSynonymDecl! decl in synonymDecls) {
+ foreach (TypeSynonymDecl/*!*/ decl in synonymDecls) {
+ Contract.Assert(decl != null);
if (!resolved.Contains(decl) &&
- forall{TypeSynonymDecl! d in deps[decl]; resolved.Contains(d)}) {
+ Contract.ForAll(deps[decl], d => resolved.Contains(d))) {
decl.Resolve(rc);
resolved.Add(decl);
}
@@ -924,12 +1025,13 @@ namespace Microsoft.Boogie unresolved = newUnresolved;
} else {
// there have to be cycles in the definitions
- foreach (TypeSynonymDecl! decl in synonymDecls) {
+ foreach (TypeSynonymDecl/*!*/ decl in synonymDecls) {
+ Contract.Assert(decl != null);
if (!resolved.Contains(decl)) {
- rc.Error(decl,
- "type synonym could not be resolved because of cycles: {0}" +
- " (replacing body with \"bool\" to continue resolving)",
- decl.Name);
+ rc.Error(decl,
+ "type synonym could not be resolved because of cycles: {0}" +
+ " (replacing body with \"bool\" to continue resolving)",
+ decl.Name);
// we simply replace the bodies of all remaining type
// synonyms with "bool" so that resolution can continue
@@ -944,129 +1046,148 @@ namespace Microsoft.Boogie }
// determine a list of all type synonyms that occur in "type"
- private static void FindDependencies(Type! type, List<TypeSynonymDecl!>! deps,
- ResolutionContext! rc) {
+ private static void FindDependencies(Type/*!*/ type, List<TypeSynonymDecl/*!*/>/*!*/ deps, ResolutionContext/*!*/ rc) {
+ Contract.Requires(type != null);
+ Contract.Requires(cce.NonNullElements(deps));
+ Contract.Requires(rc != null);
if (type.IsVariable || type.IsBasic) {
// nothing
} else if (type.IsUnresolved) {
- UnresolvedTypeIdentifier! unresType = type.AsUnresolved;
+ UnresolvedTypeIdentifier/*!*/ unresType = type.AsUnresolved;
+ Contract.Assert(unresType != null);
TypeSynonymDecl dep = rc.LookUpTypeSynonym(unresType.Name);
if (dep != null)
deps.Add(dep);
- foreach (Type! subtype in unresType.Arguments)
+ foreach (Type/*!*/ subtype in unresType.Arguments) {
+ Contract.Assert(subtype != null);
FindDependencies(subtype, deps, rc);
+ }
} else if (type.IsMap) {
- MapType! mapType = type.AsMap;
- foreach (Type! subtype in mapType.Arguments)
+ MapType/*!*/ mapType = type.AsMap;
+ Contract.Assert(mapType != null);
+ foreach (Type/*!*/ subtype in mapType.Arguments) {
+ Contract.Assert(subtype != null);
FindDependencies(subtype, deps, rc);
+ }
FindDependencies(mapType.Result, deps, rc);
} else if (type.IsCtor) {
// this can happen because we allow types to be resolved multiple times
- CtorType! ctorType = type.AsCtor;
- foreach (Type! subtype in ctorType.Arguments)
+ CtorType/*!*/ ctorType = type.AsCtor;
+ Contract.Assert(ctorType != null);
+ foreach (Type/*!*/ subtype in ctorType.Arguments) {
+ Contract.Assert(subtype != null);
FindDependencies(subtype, deps, rc);
+ }
} else {
System.Diagnostics.Debug.Fail("Did not expect this type during resolution: "
+ 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.VisitTypeSynonymDecl(this);
}
}
+ public abstract class Variable : NamedDeclaration, AI.IVariable {
+ public TypedIdent/*!*/ TypedIdent;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(TypedIdent != null);
+ }
- public abstract class Variable : NamedDeclaration, AI.IVariable
- {
- public TypedIdent! TypedIdent;
- public Variable(IToken! tok, TypedIdent! typedIdent)
- : base(tok, typedIdent.Name)
- {
+ public Variable(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent)
+ : base(tok, typedIdent.Name) {
+ Contract.Requires(tok != null);
+ Contract.Requires(typedIdent != null);
this.TypedIdent = typedIdent;
// base(tok, typedIdent.Name);
}
- public Variable(IToken! tok, TypedIdent! typedIdent, QKeyValue kv)
- : base(tok, typedIdent.Name)
- {
+ public Variable(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent, QKeyValue kv)
+ : base(tok, typedIdent.Name) {
+ Contract.Requires(tok != null);
+ Contract.Requires(typedIdent != null);
this.TypedIdent = typedIdent;
// base(tok, typedIdent.Name);
this.Attributes = kv;
}
- public abstract bool IsMutable
- {
+ public abstract bool IsMutable {
get;
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+ Contract.Requires(stream != null);
stream.Write(this, level, "var ");
EmitAttributes(stream);
EmitVitals(stream, level);
stream.WriteLine(";");
}
- public void EmitVitals(TokenTextWriter! stream, int level)
- {
- if (CommandLineOptions.Clo.PrintWithUniqueASTIds && this.TypedIdent.HasName)
- {
+ public void EmitVitals(TokenTextWriter stream, int level) {
+ Contract.Requires(stream != null);
+ if (CommandLineOptions.Clo.PrintWithUniqueASTIds && this.TypedIdent.HasName) {
stream.Write("h{0}^^", this.GetHashCode()); // the idea is that this will prepend the name printed by TypedIdent.Emit
}
this.TypedIdent.Emit(stream);
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ Contract.Requires(rc != null);
this.TypedIdent.Resolve(rc);
}
- public void ResolveWhere(ResolutionContext! rc)
- {
+ public void ResolveWhere(ResolutionContext rc) {
+ Contract.Requires(rc != null);
if (this.TypedIdent.WhereExpr != null) {
this.TypedIdent.WhereExpr.Resolve(rc);
}
ResolveAttributes(rc);
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ Contract.Requires(tc != null);
TypecheckAttributes(tc);
this.TypedIdent.Typecheck(tc);
}
[Pure]
- public object DoVisit(AI.ExprVisitor! visitor)
- {
+ public object DoVisit(AI.ExprVisitor visitor) {
+ Contract.Requires(visitor != null);
return visitor.VisitVariable(this);
}
}
- public class VariableComparer : IComparer
- {
+ public class VariableComparer : IComparer {
public int Compare(object a, object b) {
- Variable A = a as Variable;
- Variable B = b as Variable;
- if (A == null || B == null) {
- throw new ArgumentException("VariableComparer works only on objects of type Variable");
- }
- return ((!)A.Name).CompareTo(B.Name);
+ Variable A = a as Variable;
+ Variable B = b as Variable;
+ if (A == null || B == null) {
+ throw new ArgumentException("VariableComparer works only on objects of type Variable");
+ }
+ return cce.NonNull(A.Name).CompareTo(B.Name);
}
}
// class to specify the <:-parents of the values of constants
public class ConstantParent {
- public readonly IdentifierExpr! Parent;
+ public readonly IdentifierExpr/*!*/ Parent;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Parent != null);
+ }
+
// if true, the sub-dag underneath this constant-parent edge is
// disjoint from all other unique sub-dags
public readonly bool Unique;
- public ConstantParent(IdentifierExpr! parent, bool unique) {
+ public ConstantParent(IdentifierExpr parent, bool unique) {
+ Contract.Requires(parent != null);
Parent = parent;
Unique = unique;
}
}
- public class Constant : Variable
- {
+ public class Constant : Variable {
// when true, the value of this constant is meant to be distinct
// from all other constants.
public readonly bool Unique;
@@ -1074,65 +1195,73 @@ namespace Microsoft.Boogie // the <:-parents of the value of this constant. If the field is
// null, no information about the parents is provided, which means
// that the parental situation is unconstrained.
- public readonly List<ConstantParent!> Parents;
+ public readonly List<ConstantParent/*!*/> Parents;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(Parents, true));
+ }
+
// if true, it is assumed that the immediate <:-children of the
// value of this constant are completely specified
public readonly bool ChildrenComplete;
- public Constant(IToken! tok, TypedIdent! typedIdent)
- : base(tok, typedIdent)
- requires typedIdent.Name != null && typedIdent.Name.Length > 0;
- requires typedIdent.WhereExpr == null;
- {
+ public Constant(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent)
+ : base(tok, typedIdent) {
+ Contract.Requires(tok != null);
+ Contract.Requires(typedIdent != null);
+ Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0);
+ Contract.Requires(typedIdent.WhereExpr == null);
// base(tok, typedIdent);
this.Unique = true;
this.Parents = null;
this.ChildrenComplete = false;
}
- public Constant(IToken! tok, TypedIdent! typedIdent, bool unique)
- : base(tok, typedIdent)
- requires typedIdent.Name != null && typedIdent.Name.Length > 0;
- requires typedIdent.WhereExpr == null;
- {
+ public Constant(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent, bool unique)
+ : base(tok, typedIdent) {
+ Contract.Requires(tok != null);
+ Contract.Requires(typedIdent != null);
+ Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0);
+ Contract.Requires(typedIdent.WhereExpr == null);
// base(tok, typedIdent);
this.Unique = unique;
this.Parents = null;
this.ChildrenComplete = false;
}
- public Constant(IToken! tok, TypedIdent! typedIdent,
+ public Constant(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent,
bool unique,
- List<ConstantParent!> parents, bool childrenComplete,
+ List<ConstantParent/*!*/> parents, bool childrenComplete,
QKeyValue kv)
- : base(tok, typedIdent, kv)
- requires typedIdent.Name != null && typedIdent.Name.Length > 0;
- requires typedIdent.WhereExpr == null;
- {
+ : base(tok, typedIdent, kv) {
+ Contract.Requires(tok != null);
+ Contract.Requires(typedIdent != null);
+ Contract.Requires(parents == null || cce.NonNullElements(parents));
+ Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0);
+ Contract.Requires(typedIdent.WhereExpr == null);
// base(tok, typedIdent);
this.Unique = unique;
this.Parents = parents;
this.ChildrenComplete = childrenComplete;
}
- public override bool IsMutable
- {
- get
- {
+ public override bool IsMutable {
+ get {
return false;
}
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
stream.Write(this, level, "const ");
EmitAttributes(stream);
- if (this.Unique){
+ if (this.Unique) {
stream.Write(this, level, "unique ");
}
EmitVitals(stream, level);
if (Parents != null || ChildrenComplete) {
stream.Write(this, level, " extends");
- string! sep = " ";
- foreach (ConstantParent! p in (!)Parents) {
+ string/*!*/ sep = " ";
+ foreach (ConstantParent/*!*/ p in cce.NonNull(Parents)) {
+ Contract.Assert(p != null);
stream.Write(this, level, sep);
sep = ", ";
if (p.Unique)
@@ -1142,18 +1271,19 @@ namespace Microsoft.Boogie if (ChildrenComplete)
stream.Write(this, level, " complete");
}
-
+
stream.WriteLine(";");
}
- public override void Register(ResolutionContext! rc)
- {
+ public override void Register(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
rc.AddVariable(this, true);
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
base.Resolve(rc);
if (Parents != null) {
- foreach (ConstantParent! p in Parents) {
+ foreach (ConstantParent/*!*/ p in Parents) {
+ Contract.Assert(p != null);
p.Parent.Resolve(rc);
if (p.Parent.Decl != null && !(p.Parent.Decl is Constant))
rc.Error(p.Parent, "the parent of a constant has to be a constant");
@@ -1169,7 +1299,7 @@ namespace Microsoft.Boogie if (Parents[i].Parent.Decl != null) {
for (int j = i + 1; j < Parents.Count; ++j) {
if (Parents[j].Parent.Decl != null &&
- ((!)Parents[i].Parent.Decl).Equals(Parents[j].Parent.Decl))
+ cce.NonNull(Parents[i].Parent.Decl).Equals(Parents[j].Parent.Decl))
rc.Error(Parents[j].Parent,
"{0} occurs more than once as parent",
Parents[j].Parent.Decl);
@@ -1178,14 +1308,15 @@ namespace Microsoft.Boogie }
}
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
base.Typecheck(tc);
if (Parents != null) {
- foreach (ConstantParent! p in Parents) {
+ foreach (ConstantParent/*!*/ p in Parents) {
+ Contract.Assert(p != null);
p.Parent.Typecheck(tc);
- if (!((!)p.Parent.Decl).TypedIdent.Type.Unify(this.TypedIdent.Type))
+ if (!cce.NonNull(p.Parent.Decl).TypedIdent.Type.Unify(this.TypedIdent.Type))
tc.Error(p.Parent,
"parent of constant has incompatible type ({0} instead of {1})",
p.Parent.Decl.TypedIdent.Type, this.TypedIdent.Type);
@@ -1193,55 +1324,54 @@ 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.VisitConstant(this);
}
}
- public class GlobalVariable : Variable
- {
- public GlobalVariable(IToken! tok, TypedIdent! typedIdent)
- : base(tok, typedIdent)
- {
- }
- public GlobalVariable(IToken! tok, TypedIdent! typedIdent, QKeyValue kv)
- : base(tok, typedIdent, kv)
- {
- }
- public override bool IsMutable
- {
- get
- {
+ public class GlobalVariable : Variable {
+ public GlobalVariable(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent)
+ : base(tok, typedIdent) {
+ Contract.Requires(tok != null);
+ Contract.Requires(typedIdent != null);
+ }
+ public GlobalVariable(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent, QKeyValue kv)
+ : base(tok, typedIdent, kv) {
+ Contract.Requires(tok != null);
+ Contract.Requires(typedIdent != null);
+ }
+ public override bool IsMutable {
+ get {
return true;
}
}
- public override void Register(ResolutionContext! rc)
- {
+ public override void Register(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
rc.AddVariable(this, true);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitGlobalVariable(this);
}
}
- public class Formal : Variable
- {
+ public class Formal : Variable {
public bool InComing;
- public Formal(IToken! tok, TypedIdent! typedIdent, bool incoming)
- : base(tok, typedIdent)
- {
+ public Formal(IToken tok, TypedIdent typedIdent, bool incoming)
+ : base(tok, typedIdent) {
+ Contract.Requires(typedIdent != null);
+ Contract.Requires(tok != null);
InComing = incoming;
}
- public override bool IsMutable
- {
- get
- {
+ public override bool IsMutable {
+ get {
return !InComing;
}
}
- public override void Register(ResolutionContext! rc)
- {
+ public override void Register(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
rc.AddVariable(this, false);
}
@@ -1249,10 +1379,12 @@ namespace Microsoft.Boogie /// Given a sequence of Formal declarations, returns sequence of Formals like the given one but without where clauses.
/// The Type of each Formal is cloned.
/// </summary>
- public static VariableSeq! StripWhereClauses(VariableSeq! w)
- {
+ public static VariableSeq StripWhereClauses(VariableSeq w) {
+ Contract.Requires(w != null);
+ Contract.Ensures(Contract.Result<VariableSeq>() != null);
VariableSeq s = new VariableSeq();
- foreach (Variable! v in w) {
+ foreach (Variable/*!*/ v in w) {
+ Contract.Assert(v != null);
Formal f = (Formal)v;
TypedIdent ti = f.TypedIdent;
s.Add(new Formal(f.tok, new TypedIdent(ti.tok, ti.Name, ti.Type.CloneUnresolved()), f.InComing));
@@ -1260,115 +1392,124 @@ namespace Microsoft.Boogie return s;
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitFormal(this);
}
}
- public class LocalVariable : Variable
- {
- public LocalVariable(IToken! tok, TypedIdent! typedIdent, QKeyValue kv)
- {
- base(tok, typedIdent, kv);
- }
- public LocalVariable(IToken! tok, TypedIdent! typedIdent)
- {
- base(tok, typedIdent, null);
- }
- public override bool IsMutable
- {
- get
- {
+ public class LocalVariable : Variable {
+ public LocalVariable(IToken tok, TypedIdent typedIdent, QKeyValue kv)
+ : base(tok, typedIdent, kv) {//BASEMOVEA
+ Contract.Requires(typedIdent != null);
+ Contract.Requires(tok != null);
+ //:base(tok, typedIdent, kv);
+ }
+ public LocalVariable(IToken tok, TypedIdent typedIdent)
+ : base(tok, typedIdent, null) {//BASEMOVEA
+ Contract.Requires(typedIdent != null);
+ Contract.Requires(tok != null);
+ //:base(tok, typedIdent, null);
+ }
+ public override bool IsMutable {
+ get {
return true;
}
}
- public override void Register(ResolutionContext! rc)
- {
+ public override void Register(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
rc.AddVariable(this, false);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitLocalVariable(this);
}
}
- public class Incarnation : LocalVariable
- {
+ public class Incarnation : LocalVariable {
public int incarnationNumber;
- public Incarnation(Variable! var, int i) :
+ public Incarnation(Variable/*!*/ var, int i) :
base(
var.tok,
- new TypedIdent(var.TypedIdent.tok,var.TypedIdent.Name + "@" + i,var.TypedIdent.Type)
- )
- {
+ new TypedIdent(var.TypedIdent.tok, var.TypedIdent.Name + "@" + i, var.TypedIdent.Type)
+ ) {
+ Contract.Requires(var != null);
incarnationNumber = i;
}
}
- public class BoundVariable : Variable
- {
- public BoundVariable(IToken! tok, TypedIdent! typedIdent)
- requires typedIdent.WhereExpr == null;
- {
- base(tok, typedIdent); // here for aesthetic reasons
- }
- public override bool IsMutable
- {
- get
- {
+ public class BoundVariable : Variable {
+ public BoundVariable(IToken tok, TypedIdent typedIdent)
+ : base(tok, typedIdent) {//BASEMOVEA
+ Contract.Requires(typedIdent != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(typedIdent.WhereExpr == null);
+ //:base(tok, typedIdent); // here for aesthetic reasons
+ }
+ public override bool IsMutable {
+ get {
return false;
}
}
- public override void Register(ResolutionContext! rc)
- {
+ public override void Register(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
rc.AddVariable(this, false);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitBoundVariable(this);
}
}
- public abstract class DeclWithFormals : NamedDeclaration
- {
- public TypeVariableSeq! TypeParameters;
- public /*readonly--except in StandardVisitor*/ VariableSeq! InParams, OutParams;
-
- public DeclWithFormals (IToken! tok, string! name, TypeVariableSeq! typeParams,
- VariableSeq! inParams, VariableSeq! outParams)
- : base(tok, name)
- {
+ public abstract class DeclWithFormals : NamedDeclaration {
+ public TypeVariableSeq/*!*/ TypeParameters;
+ public /*readonly--except in StandardVisitor*/ VariableSeq/*!*/ InParams, OutParams;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(TypeParameters != null);
+ Contract.Invariant(InParams != null);
+ Contract.Invariant(OutParams != null);
+ }
+
+ public DeclWithFormals(IToken tok, string name, TypeVariableSeq typeParams,
+ VariableSeq inParams, VariableSeq outParams)
+ : base(tok, name) {
+ Contract.Requires(inParams != null);
+ Contract.Requires(outParams != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(name != null);
+ Contract.Requires(tok != null);
this.TypeParameters = typeParams;
this.InParams = inParams;
this.OutParams = outParams;
// base(tok, name);
}
- protected DeclWithFormals (DeclWithFormals! that)
- : base(that.tok, (!) that.Name)
- {
+ protected DeclWithFormals(DeclWithFormals that)
+ : base(that.tok, cce.NonNull(that.Name)) {
+ Contract.Requires(that != null);
this.TypeParameters = that.TypeParameters;
this.InParams = that.InParams;
this.OutParams = that.OutParams;
// base(that.tok, (!) that.Name);
}
- protected void EmitSignature (TokenTextWriter! stream, bool shortRet)
- {
+ protected void EmitSignature(TokenTextWriter stream, bool shortRet) {
+ Contract.Requires(stream != null);
Type.EmitOptionalTypeParams(stream, TypeParameters);
stream.Write("(");
InParams.Emit(stream);
stream.Write(")");
- if (shortRet)
- {
- assert OutParams.Length == 1;
+ if (shortRet) {
+ Contract.Assert(OutParams.Length == 1);
stream.Write(" : ");
- ((!)OutParams[0]).TypedIdent.Type.Emit(stream);
- }
- else if (OutParams.Length > 0)
- {
+ cce.NonNull(OutParams[0]).TypedIdent.Type.Emit(stream);
+ } else if (OutParams.Length > 0) {
stream.Write(" returns (");
OutParams.Emit(stream);
stream.Write(")");
@@ -1376,13 +1517,17 @@ namespace Microsoft.Boogie }
// Register all type parameters at the resolution context
- protected void RegisterTypeParameters(ResolutionContext! rc) {
- foreach (TypeVariable! v in TypeParameters)
+ protected void RegisterTypeParameters(ResolutionContext rc) {
+ Contract.Requires(rc != null);
+ foreach (TypeVariable/*!*/ v in TypeParameters) {
+ Contract.Assert(v != null);
rc.AddTypeBinder(v);
+ }
}
protected void SortTypeParams() {
- TypeSeq! allTypes = InParams.ToTypeSeq;
+ TypeSeq/*!*/ allTypes = InParams.ToTypeSeq;
+ Contract.Assert(allTypes != null);
allTypes.AddRange(OutParams.ToTypeSeq);
TypeParameters = Type.SortTypeParams(TypeParameters, allTypes, null);
}
@@ -1395,12 +1540,12 @@ namespace Microsoft.Boogie /// context.
/// </summary>
/// <param name="rc"></param>
- protected void RegisterFormals(VariableSeq! formals, ResolutionContext! rc)
- {
- foreach (Formal! f in formals)
- {
- if (f.Name != TypedIdent.NoName)
- {
+ protected void RegisterFormals(VariableSeq formals, ResolutionContext rc) {
+ Contract.Requires(rc != null);
+ Contract.Requires(formals != null);
+ foreach (Formal/*!*/ f in formals) {
+ Contract.Assert(f != null);
+ if (f.Name != TypedIdent.NoName) {
rc.AddVariable(f, false);
}
f.Resolve(rc);
@@ -1411,34 +1556,47 @@ namespace Microsoft.Boogie /// Resolves the where clauses (and attributes) of the formals.
/// </summary>
/// <param name="rc"></param>
- protected void ResolveFormals(VariableSeq! formals, ResolutionContext! rc)
- {
- foreach (Formal! f in formals)
- {
+ protected void ResolveFormals(VariableSeq formals, ResolutionContext rc) {
+ Contract.Requires(rc != null);
+ Contract.Requires(formals != null);
+ foreach (Formal/*!*/ f in formals) {
+ Contract.Assert(f != null);
f.ResolveWhere(rc);
}
}
- public override void Typecheck(TypecheckingContext! tc) {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
TypecheckAttributes(tc);
- foreach (Formal! p in InParams) {
+ foreach (Formal/*!*/ p in InParams) {
+ Contract.Assert(p != null);
p.Typecheck(tc);
}
- foreach (Formal! p in OutParams) {
+ foreach (Formal/*!*/ p in OutParams) {
+ Contract.Assert(p != null);
p.Typecheck(tc);
}
}
}
public class Expansion {
- public string? ignore; // when to ignore
- public Expr! body;
- public TypeVariableSeq! TypeParameters;
- public Variable[]! formals;
-
- public Expansion(string? ignore, Expr! body,
- TypeVariableSeq! typeParams, Variable[]! formals)
- {
+ public string ignore; // when to ignore
+ public Expr/*!*/ body;
+ public TypeVariableSeq/*!*/ TypeParameters;
+ public Variable[]/*!*/ formals;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(body != null);
+ Contract.Invariant(TypeParameters != null);
+ Contract.Invariant(formals != null);
+ }
+
+
+ public Expansion(string ignore, Expr body,
+ TypeVariableSeq/*!*/ typeParams, Variable[] formals) {
+ Contract.Requires(typeParams != null);
+ Contract.Requires(formals != null);
+ Contract.Requires(body != null);
this.ignore = ignore;
this.body = body;
this.TypeParameters = typeParams;
@@ -1446,46 +1604,70 @@ namespace Microsoft.Boogie }
}
- public class Function : DeclWithFormals
- {
- public string? Comment;
+ public class Function : DeclWithFormals {
+ public string Comment;
// the body is only set if the function is declared with {:expand true}
public Expr Body;
- public List<Expansion!>? expansions;
+ public List<Expansion/*!*/> expansions;
public bool doingExpansion;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(expansions, true));
+ }
+
private bool neverTrigger;
private bool neverTriggerComputed;
- public Function(IToken! tok, string! name, VariableSeq! args, Variable! result)
- {
- this(tok, name, new TypeVariableSeq(), args, result, null);
- }
- public Function(IToken! tok, string! name, TypeVariableSeq! typeParams, VariableSeq! args, Variable! result)
- {
- this(tok, name, typeParams, args, result, null);
- }
- public Function(IToken! tok, string! name, VariableSeq! args, Variable! result,
- string? comment)
- {
- this(tok, name, new TypeVariableSeq(), args, result, comment);
- }
- public Function(IToken! tok, string! name, TypeVariableSeq! typeParams, VariableSeq! args, Variable! result,
- string? comment)
- : base(tok, name, typeParams, args, new VariableSeq(result))
- {
+ public Function(IToken tok, string name, VariableSeq args, Variable result)
+ : this(tok, name, new TypeVariableSeq(), args, result, null) {
+ Contract.Requires(result != null);
+ Contract.Requires(args != null);
+ Contract.Requires(name != null);
+ Contract.Requires(tok != null);
+ //:this(tok, name, new TypeVariableSeq(), args, result, null);
+ }
+ public Function(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq args, Variable result)
+ : this(tok, name, typeParams, args, result, null) {
+ Contract.Requires(result != null);
+ Contract.Requires(args != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(name != null);
+ Contract.Requires(tok != null);
+ //:this(tok, name, typeParams, args, result, null);
+ }
+ public Function(IToken tok, string name, VariableSeq args, Variable result, string comment)
+ : this(tok, name, new TypeVariableSeq(), args, result, comment) {
+ Contract.Requires(result != null);
+ Contract.Requires(args != null);
+ Contract.Requires(name != null);
+ Contract.Requires(tok != null);
+ //:this(tok, name, new TypeVariableSeq(), args, result, comment);
+ }
+ public Function(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq args, Variable/*!*/ result, string comment)
+ : base(tok, name, typeParams, args, new VariableSeq(result)) {
+ Contract.Requires(result != null);
+ Contract.Requires(args != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(name != null);
+ Contract.Requires(tok != null);
Comment = comment;
// base(tok, name, args, new VariableSeq(result));
}
- public Function(IToken! tok, string! name, TypeVariableSeq! typeParams, VariableSeq! args, Variable! result,
- string? comment, QKeyValue kv)
- {
- this(tok, name, typeParams, args, result, comment);
+ public Function(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq args, Variable result,
+ string comment, QKeyValue kv)
+ : this(tok, name, typeParams, args, result, comment) {
+ Contract.Requires(args != null);
+ Contract.Requires(result != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(name != null);
+ Contract.Requires(tok != null);
+ //:this(tok, name, typeParams, args, result, comment);
this.Attributes = kv;
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
if (Comment != null) {
stream.WriteLine(this, level, "// " + Comment);
}
@@ -1500,7 +1682,7 @@ namespace Microsoft.Boogie if (Body != null) {
stream.WriteLine();
stream.WriteLine("{");
- stream.Write(level+1, "");
+ stream.Write(level + 1, "");
Body.Emit(stream);
stream.WriteLine();
stream.WriteLine("}");
@@ -1508,12 +1690,12 @@ namespace Microsoft.Boogie stream.WriteLine(";");
}
}
- public override void Register(ResolutionContext! rc)
- {
+ public override void Register(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
rc.AddProcedure(this);
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
int previousTypeBinderState = rc.TypeBinderState;
try {
RegisterTypeParameters(rc);
@@ -1533,22 +1715,21 @@ namespace Microsoft.Boogie }
SortTypeParams();
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
// PR: why was the base call left out previously?
base.Typecheck(tc);
// TypecheckAttributes(tc);
if (Body != null) {
Body.Typecheck(tc);
- if (!((!)Body.Type).Unify(((!)OutParams[0]).TypedIdent.Type))
+ if (!cce.NonNull(Body.Type).Unify(cce.NonNull(OutParams[0]).TypedIdent.Type))
tc.Error(Body,
"function body with invalid type: {0} (expected: {1})",
- Body.Type, ((!)OutParams[0]).TypedIdent.Type);
+ Body.Type, cce.NonNull(OutParams[0]).TypedIdent.Type);
}
}
- public bool NeverTrigger
- {
+ public bool NeverTrigger {
get {
if (!neverTriggerComputed) {
this.CheckBooleanAttribute("never_pattern", ref neverTrigger);
@@ -1558,30 +1739,44 @@ 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.VisitFunction(this);
}
}
- public class Requires : Absy, IPotentialErrorNode
- {
+ public class Requires : Absy, IPotentialErrorNode {
public readonly bool Free;
- public Expr! Condition;
- public string? Comment;
+ public Expr/*!*/ Condition;
+ public string Comment;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Condition != null);
+ Contract.Invariant(errorData == null || errorData is string);
+ }
+
// TODO: convert to use generics
private object errorData;
public object ErrorData {
- get { return errorData; }
- set { errorData = value; }
+ get {
+ return errorData;
+ }
+ set {
+ errorData = value;
+ }
}
- invariant errorData != null ==> errorData is string;
+
private MiningStrategy errorDataEnhanced;
public MiningStrategy ErrorDataEnhanced {
- get { return errorDataEnhanced; }
- set { errorDataEnhanced = value; }
+ get {
+ return errorDataEnhanced;
+ }
+ set {
+ errorDataEnhanced = value;
+ }
}
public QKeyValue Attributes;
@@ -1592,9 +1787,10 @@ namespace Microsoft.Boogie }
}
- public Requires(IToken! token, bool free, Expr! condition, string? comment, QKeyValue kv)
- : base(token)
- {
+ public Requires(IToken token, bool free, Expr condition, string comment, QKeyValue kv)
+ : base(token) {
+ Contract.Requires(condition != null);
+ Contract.Requires(token != null);
this.Free = free;
this.Condition = condition;
this.Comment = comment;
@@ -1602,23 +1798,27 @@ namespace Microsoft.Boogie // base(token);
}
- public Requires(IToken! token, bool free, Expr! condition, string? comment)
- {
- this(token, free, condition, comment, null);
+ public Requires(IToken token, bool free, Expr condition, string comment)
+ : this(token, free, condition, comment, null) {
+ Contract.Requires(condition != null);
+ Contract.Requires(token != null);
+ //:this(token, free, condition, comment, null);
}
- public Requires(bool free, Expr! condition)
- {
- this(Token.NoToken, free, condition, null);
+ public Requires(bool free, Expr condition)
+ : this(Token.NoToken, free, condition, null) {
+ Contract.Requires(condition != null);
+ //:this(Token.NoToken, free, condition, null);
}
- public Requires(bool free, Expr! condition, string? comment)
- {
- this(Token.NoToken, free, condition, comment);
+ public Requires(bool free, Expr condition, string comment)
+ : this(Token.NoToken, free, condition, comment) {
+ Contract.Requires(condition != null);
+ //:this(Token.NoToken, free, condition, comment);
}
- public void Emit(TokenTextWriter! stream, int level)
- {
+ public void Emit(TokenTextWriter stream, int level) {
+ Contract.Requires(stream != null);
if (Comment != null) {
stream.WriteLine(this, level, "// " + Comment);
}
@@ -1627,40 +1827,51 @@ namespace Microsoft.Boogie stream.WriteLine(";");
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
this.Condition.Resolve(rc);
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
this.Condition.Typecheck(tc);
- assert this.Condition.Type != null; // follows from postcondition of Expr.Typecheck
- if (!this.Condition.Type.Unify(Type.Bool))
- {
+ Contract.Assert(this.Condition.Type != null); // follows from postcondition of Expr.Typecheck
+ if (!this.Condition.Type.Unify(Type.Bool)) {
tc.Error(this, "preconditions must be of type bool");
}
}
}
- public class Ensures : Absy, IPotentialErrorNode
- {
+ public class Ensures : Absy, IPotentialErrorNode {
public readonly bool Free;
- public Expr! Condition;
- public string? Comment;
+ public Expr/*!*/ Condition;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Condition != null);
+ Contract.Invariant(errorData == null || errorData is string);
+ }
+
+ public string Comment;
// TODO: convert to use generics
private object errorData;
public object ErrorData {
- get { return errorData; }
- set { errorData = value; }
+ get {
+ return errorData;
+ }
+ set {
+ errorData = value;
+ }
}
- invariant errorData != null ==> errorData is string;
private MiningStrategy errorDataEnhanced;
public MiningStrategy ErrorDataEnhanced {
- get { return errorDataEnhanced; }
- set { errorDataEnhanced = value; }
+ get {
+ return errorDataEnhanced;
+ }
+ set {
+ errorDataEnhanced = value;
+ }
}
public String ErrorMessage {
@@ -1671,9 +1882,10 @@ namespace Microsoft.Boogie public QKeyValue Attributes;
- public Ensures(IToken! token, bool free, Expr! condition, string? comment, QKeyValue kv)
- : base(token)
- {
+ public Ensures(IToken token, bool free, Expr/*!*/ condition, string comment, QKeyValue kv)
+ : base(token) {
+ Contract.Requires(condition != null);
+ Contract.Requires(token != null);
this.Free = free;
this.Condition = condition;
this.Comment = comment;
@@ -1681,23 +1893,27 @@ namespace Microsoft.Boogie // base(token);
}
- public Ensures(IToken! token, bool free, Expr! condition, string? comment)
- {
- this(token, free, condition, comment, null);
+ public Ensures(IToken token, bool free, Expr condition, string comment)
+ : this(token, free, condition, comment, null) {
+ Contract.Requires(condition != null);
+ Contract.Requires(token != null);
+ //:this(token, free, condition, comment, null);
}
- public Ensures(bool free, Expr! condition)
- {
- this(Token.NoToken, free, condition, null);
+ public Ensures(bool free, Expr condition)
+ : this(Token.NoToken, free, condition, null) {
+ Contract.Requires(condition != null);
+ //:this(Token.NoToken, free, condition, null);
}
- public Ensures(bool free, Expr! condition, string? comment)
- {
- this(Token.NoToken, free, condition, comment);
+ public Ensures(bool free, Expr condition, string comment)
+ : this(Token.NoToken, free, condition, comment) {
+ Contract.Requires(condition != null);
+ //:this(Token.NoToken, free, condition, comment);
}
- public void Emit(TokenTextWriter! stream, int level)
- {
+ public void Emit(TokenTextWriter stream, int level) {
+ Contract.Requires(stream != null);
if (Comment != null) {
stream.WriteLine(this, level, "// " + Comment);
}
@@ -1706,68 +1922,73 @@ namespace Microsoft.Boogie stream.WriteLine(";");
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
this.Condition.Resolve(rc);
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
this.Condition.Typecheck(tc);
- assert this.Condition.Type != null; // follows from postcondition of Expr.Typecheck
- if (!this.Condition.Type.Unify(Type.Bool))
- {
+ Contract.Assert(this.Condition.Type != null); // follows from postcondition of Expr.Typecheck
+ if (!this.Condition.Type.Unify(Type.Bool)) {
tc.Error(this, "postconditions must be of type bool");
}
}
}
- public class Procedure : DeclWithFormals
- {
- public RequiresSeq! Requires;
- public IdentifierExprSeq! Modifies;
- public EnsuresSeq! Ensures;
+ public class Procedure : DeclWithFormals {
+ public RequiresSeq/*!*/ Requires;
+ public IdentifierExprSeq/*!*/ Modifies;
+ public EnsuresSeq/*!*/ Ensures;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Requires != null);
+ Contract.Invariant(Modifies != null);
+ Contract.Invariant(Ensures != null);
+ Contract.Invariant(Summary != null);
+ }
+
// Abstract interpretation: Procedure-specific invariants...
[Rep]
- public readonly ProcedureSummary! Summary;
-
- public Procedure (
- IToken! tok,
- string! name,
- TypeVariableSeq! typeParams,
- VariableSeq! inParams,
- VariableSeq! outParams,
- RequiresSeq! @requires,
- IdentifierExprSeq! @modifies,
- EnsuresSeq! @ensures
- )
- {
- this(tok, name, typeParams, inParams, outParams, @requires, @modifies, @ensures, null);
- }
-
- public Procedure (
- IToken! tok,
- string! name,
- TypeVariableSeq! typeParams,
- VariableSeq! inParams,
- VariableSeq! outParams,
- RequiresSeq! @requires,
- IdentifierExprSeq! @modifies,
- EnsuresSeq! @ensures,
- QKeyValue kv
+ public readonly ProcedureSummary/*!*/ Summary;
+
+ public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ inParams, VariableSeq/*!*/ outParams,
+ RequiresSeq/*!*/ requires, IdentifierExprSeq/*!*/ modifies, EnsuresSeq/*!*/ ensures)
+ : this(tok, name, typeParams, inParams, outParams, requires, modifies, ensures, null) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(inParams != null);
+ Contract.Requires(outParams != null);
+ Contract.Requires(requires != null);
+ Contract.Requires(modifies != null);
+ Contract.Requires(ensures != null);
+ //:this(tok, name, typeParams, inParams, outParams, requires, modifies, ensures, null);
+ }
+
+ public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ inParams, VariableSeq/*!*/ outParams,
+ RequiresSeq/*!*/ @requires, IdentifierExprSeq/*!*/ @modifies, EnsuresSeq/*!*/ @ensures, QKeyValue kv
)
- : base(tok, name, typeParams, inParams, outParams)
- {
+ : base(tok, name, typeParams, inParams, outParams) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(inParams != null);
+ Contract.Requires(outParams != null);
+ Contract.Requires(@requires != null);
+ Contract.Requires(@modifies != null);
+ Contract.Requires(@ensures != null);
this.Requires = @requires;
this.Modifies = @modifies;
this.Ensures = @ensures;
this.Summary = new ProcedureSummary();
this.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, "procedure ");
EmitAttributes(stream);
stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name));
@@ -1776,28 +1997,25 @@ namespace Microsoft.Boogie level++;
- foreach (Requires! e in this.Requires)
- {
+ foreach (Requires/*!*/ e in this.Requires) {
+ Contract.Assert(e != null);
e.Emit(stream, level);
}
- if (this.Modifies.Length > 0)
- {
+ if (this.Modifies.Length > 0) {
stream.Write(level, "modifies ");
this.Modifies.Emit(stream, false);
stream.WriteLine(";");
}
- foreach (Ensures! e in this.Ensures)
- {
+ foreach (Ensures/*!*/ e in this.Ensures) {
+ Contract.Assert(e != null);
e.Emit(stream, level);
}
- if (!CommandLineOptions.Clo.IntraproceduralInfer)
- {
- for (int s=0; s < this.Summary.Count; s++)
- {
- ProcedureSummaryEntry! entry = (!) this.Summary[s];
+ if (!CommandLineOptions.Clo.IntraproceduralInfer) {
+ for (int s = 0; s < this.Summary.Count; s++) {
+ ProcedureSummaryEntry/*!*/ entry = cce.NonNull(this.Summary[s]);
stream.Write(level + 1, "// ");
Expr e;
e = (Expr)entry.Lattice.ToPredicate(entry.OnEntry);
@@ -1813,16 +2031,16 @@ namespace Microsoft.Boogie stream.WriteLine();
}
- public override void Register(ResolutionContext! rc)
- {
+ public override void Register(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
rc.AddProcedure(this);
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
rc.PushVarContext();
- foreach (IdentifierExpr! ide in Modifies)
- {
+ foreach (IdentifierExpr/*!*/ ide in Modifies) {
+ Contract.Assert(ide != null);
ide.Resolve(rc);
}
@@ -1832,16 +2050,16 @@ namespace Microsoft.Boogie RegisterFormals(InParams, rc);
ResolveFormals(InParams, rc); // "where" clauses of in-parameters are resolved without the out-parameters in scope
- foreach (Requires! e in Requires)
- {
+ foreach (Requires/*!*/ e in Requires) {
+ Contract.Assert(e != null);
e.Resolve(rc);
}
RegisterFormals(OutParams, rc);
ResolveFormals(OutParams, rc); // "where" clauses of out-parameters are resolved with both in- and out-parametes in scope
-
+
rc.StateMode = ResolutionContext.State.Two;
- foreach (Ensures! e in Ensures)
- {
+ foreach (Ensures/*!*/ e in Ensures) {
+ Contract.Assert(e != null);
e.Resolve(rc);
}
rc.StateMode = ResolutionContext.State.Single;
@@ -1860,63 +2078,68 @@ namespace Microsoft.Boogie SortTypeParams();
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
base.Typecheck(tc);
- foreach (IdentifierExpr! ide in Modifies)
- {
- assume ide.Decl != null;
- if (!ide.Decl.IsMutable)
- {
+ foreach (IdentifierExpr/*!*/ ide in Modifies) {
+ Contract.Assert(ide != null);
+ Contract.Assume(ide.Decl != null);
+ if (!ide.Decl.IsMutable) {
tc.Error(this, "modifies list contains constant: {0}", ide.Name);
}
ide.Typecheck(tc);
}
- foreach (Requires! e in Requires)
- {
+ foreach (Requires/*!*/ e in Requires) {
+ Contract.Assert(e != null);
e.Typecheck(tc);
}
- foreach (Ensures! e in Ensures)
- {
+ foreach (Ensures/*!*/ e in Ensures) {
+ Contract.Assert(e != null);
e.Typecheck(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.VisitProcedure(this);
}
}
- public class Implementation : DeclWithFormals
- {
- public VariableSeq! LocVars;
- [Rep] public StmtList StructuredStmts;
- [Rep] public List<Block!>! Blocks;
+ public class Implementation : DeclWithFormals {
+ public VariableSeq/*!*/ LocVars;
+ [Rep]
+ public StmtList StructuredStmts;
+ [Rep]
+ public List<Block/*!*/>/*!*/ Blocks;
public Procedure Proc;
// Blocks before applying passification etc.
// Both are used only when /inline is set.
- public List<Block!>? OriginalBlocks;
- public VariableSeq? OriginalLocVars;
+ public List<Block/*!*/> OriginalBlocks;
+ public VariableSeq OriginalLocVars;
// Strongly connected components
- private StronglyConnectedComponents<Block!> scc;
+ private StronglyConnectedComponents<Block/*!*/> scc;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(LocVars != null);
+ Contract.Invariant(cce.NonNullElements(Blocks));
+ Contract.Invariant(cce.NonNullElements(OriginalBlocks, true));
+ Contract.Invariant(cce.NonNullElements(scc, true));
+
+ }
private bool BlockPredecessorsComputed;
- public bool StronglyConnectedComponentsComputed
- {
- get
- {
+ public bool StronglyConnectedComponentsComputed {
+ get {
return this.scc != null;
}
}
- public bool SkipVerification
- {
- get
- {
+ public bool SkipVerification {
+ get {
bool verify = true;
- ((!)this.Proc).CheckBooleanAttribute("verify", ref verify);
+ cce.NonNull(this.Proc).CheckBooleanAttribute("verify", ref verify);
this.CheckBooleanAttribute("verify", ref verify);
if (!verify) {
return true;
@@ -1924,8 +2147,9 @@ namespace Microsoft.Boogie if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert ||
CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assume) {
- Expr? inl = this.FindExprAttribute("inline");
- if (inl == null) inl = this.Proc.FindExprAttribute("inline");
+ Expr inl = this.FindExprAttribute("inline");
+ if (inl == null)
+ inl = this.Proc.FindExprAttribute("inline");
if (inl != null && inl is LiteralExpr && ((LiteralExpr)inl).isBigNum && ((LiteralExpr)inl).asBigNum.Signum > 0) {
return true;
}
@@ -1935,27 +2159,49 @@ namespace Microsoft.Boogie }
}
- public Implementation(IToken! tok, string! name, TypeVariableSeq! typeParams,
- VariableSeq! inParams, VariableSeq! outParams,
- VariableSeq! localVariables, [Captured] StmtList! structuredStmts)
- {
- this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors());
- }
-
- public Implementation(IToken! tok, string! name, TypeVariableSeq! typeParams,
- VariableSeq! inParams, VariableSeq! outParams,
- VariableSeq! localVariables, [Captured] StmtList! structuredStmts,
- Errors! errorHandler)
- {
- this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, errorHandler);
- }
-
- public Implementation(IToken! tok, string! name, TypeVariableSeq! typeParams,
- VariableSeq! inParams, VariableSeq! outParams,
- VariableSeq! localVariables, [Captured] StmtList! structuredStmts, QKeyValue kv,
- Errors! errorHandler)
- : base(tok, name, typeParams, inParams, outParams)
- {
+ public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] StmtList structuredStmts)
+ : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()) {
+ Contract.Requires(structuredStmts != null);
+ Contract.Requires(localVariables != null);
+ Contract.Requires(outParams != null);
+ Contract.Requires(inParams != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(name != null);
+ Contract.Requires(tok != null);
+ //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors());
+ }
+
+ public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] StmtList structuredStmts, Errors errorHandler)
+ : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, errorHandler) {
+ Contract.Requires(errorHandler != null);
+ Contract.Requires(structuredStmts != null);
+ Contract.Requires(localVariables != null);
+ Contract.Requires(outParams != null);
+ Contract.Requires(inParams != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(name != null);
+ Contract.Requires(tok != null);
+ //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, errorHandler);
+ }
+
+ public Implementation(IToken/*!*/ tok,
+ string/*!*/ name,
+ TypeVariableSeq/*!*/ typeParams,
+ VariableSeq/*!*/ inParams,
+ VariableSeq/*!*/ outParams,
+ VariableSeq/*!*/ localVariables,
+ [Captured] StmtList/*!*/ structuredStmts,
+ QKeyValue kv,
+ Errors/*!*/ errorHandler)
+ : base(tok, name, typeParams, inParams, outParams) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(inParams != null);
+ Contract.Requires(outParams != null);
+ Contract.Requires(localVariables != null);
+ Contract.Requires(structuredStmts != null);
+ Contract.Requires(errorHandler != null);
LocVars = localVariables;
StructuredStmts = structuredStmts;
BigBlocksResolutionContext ctx = new BigBlocksResolutionContext(structuredStmts, errorHandler);
@@ -1967,18 +2213,32 @@ namespace Microsoft.Boogie // base(tok, name, inParams, outParams);
}
- public Implementation(IToken! tok, string! name, TypeVariableSeq! typeParams,
- VariableSeq! inParams, VariableSeq! outParams,
- VariableSeq! localVariables, [Captured] List<Block!>! block)
- {
- this(tok, name, typeParams, inParams, outParams, localVariables, block, null);
- }
-
- public Implementation(IToken! tok, string! name, TypeVariableSeq! typeParams,
- VariableSeq! inParams, VariableSeq! outParams,
- VariableSeq! localVariables, [Captured] List<Block!>! blocks, QKeyValue kv)
- : base(tok, name, typeParams, inParams, outParams)
- {
+ public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] List<Block/*!*/> block)
+ : this(tok, name, typeParams, inParams, outParams, localVariables, block, null) {
+ Contract.Requires(cce.NonNullElements(block));
+ Contract.Requires(localVariables != null);
+ Contract.Requires(outParams != null);
+ Contract.Requires(inParams != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(name != null);
+ Contract.Requires(tok != null);
+ //:this(tok, name, typeParams, inParams, outParams, localVariables, block, null);
+ }
+
+ public Implementation(IToken/*!*/ tok,
+ string/*!*/ name,
+ TypeVariableSeq/*!*/ typeParams,
+ VariableSeq/*!*/ inParams,
+ VariableSeq/*!*/ outParams,
+ VariableSeq/*!*/ localVariables,
+ [Captured] List<Block/*!*/>/*!*/ blocks,
+ QKeyValue kv)
+ : base(tok, name, typeParams, inParams, outParams) {
+ Contract.Requires(name != null);
+ Contract.Requires(inParams != null);
+ Contract.Requires(outParams != null);
+ Contract.Requires(localVariables != null);
+ Contract.Requires(cce.NonNullElements(blocks));
LocVars = localVariables;
Blocks = blocks;
BlockPredecessorsComputed = false;
@@ -1988,8 +2248,8 @@ namespace Microsoft.Boogie //base(tok, name, inParams, outParams);
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
stream.Write(this, level, "implementation ");
EmitAttributes(stream);
stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name));
@@ -1998,7 +2258,8 @@ namespace Microsoft.Boogie stream.WriteLine(level, "{0}", '{');
- foreach (Variable! v in this.LocVars) {
+ foreach (Variable/*!*/ v in this.LocVars) {
+ Contract.Assert(v != null);
v.Emit(stream, level + 1);
}
@@ -2008,21 +2269,19 @@ namespace Microsoft.Boogie }
if (CommandLineOptions.Clo.PrintUnstructured < 2) {
if (CommandLineOptions.Clo.PrintUnstructured == 1) {
- stream.WriteLine(this, level+1, "/*** structured program:");
+ stream.WriteLine(this, level + 1, "/*** structured program:");
}
- this.StructuredStmts.Emit(stream, level+1);
+ this.StructuredStmts.Emit(stream, level + 1);
if (CommandLineOptions.Clo.PrintUnstructured == 1) {
- stream.WriteLine(level+1, "**** end structured program */");
+ stream.WriteLine(level + 1, "**** end structured program */");
}
}
}
if (this.StructuredStmts == null || 1 <= CommandLineOptions.Clo.PrintUnstructured ||
- CommandLineOptions.Clo.PrintInstrumented || CommandLineOptions.Clo.PrintInlined)
- {
- foreach (Block b in this.Blocks)
- {
- b.Emit(stream, level+1);
+ CommandLineOptions.Clo.PrintInstrumented || CommandLineOptions.Clo.PrintInlined) {
+ foreach (Block b in this.Blocks) {
+ b.Emit(stream, level + 1);
}
}
@@ -2031,25 +2290,21 @@ namespace Microsoft.Boogie stream.WriteLine();
stream.WriteLine();
}
- public override void Register(ResolutionContext! rc)
- {
+ public override void Register(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
// nothing to register
}
- 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;
}
- DeclWithFormals dwf = rc.LookUpProcedure((!) this.Name);
+ DeclWithFormals dwf = rc.LookUpProcedure(cce.NonNull(this.Name));
Proc = dwf as Procedure;
- if (dwf == null)
- {
+ if (dwf == null) {
rc.Error(this, "implementation given for undeclared procedure: {0}", this.Name);
- }
- else if (Proc == null)
- {
+ } else if (Proc == null) {
rc.Error(this, "implementations given for function, not procedure: {0}", this.Name);
}
@@ -2061,31 +2316,29 @@ namespace Microsoft.Boogie RegisterFormals(InParams, rc);
RegisterFormals(OutParams, rc);
- foreach (Variable! v in LocVars)
- {
+ foreach (Variable/*!*/ v in LocVars) {
+ Contract.Assert(v != null);
v.Register(rc);
v.Resolve(rc);
}
- foreach (Variable! v in LocVars)
- {
+ foreach (Variable/*!*/ v in LocVars) {
+ Contract.Assert(v != null);
v.ResolveWhere(rc);
}
rc.PushProcedureContext();
- foreach (Block b in Blocks)
- {
+ foreach (Block b in Blocks) {
b.Register(rc);
}
-
+
ResolveAttributes(rc);
rc.StateMode = ResolutionContext.State.Two;
- foreach (Block b in Blocks)
- {
+ foreach (Block b in Blocks) {
b.Resolve(rc);
}
rc.StateMode = ResolutionContext.State.Single;
-
+
rc.PopProcedureContext();
rc.PopVarContext();
@@ -2098,11 +2351,11 @@ namespace Microsoft.Boogie }
SortTypeParams();
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
base.Typecheck(tc);
- assume this.Proc != null;
+ Contract.Assume(this.Proc != null);
if (this.TypeParameters.Length != Proc.TypeParameters.Length) {
tc.Error(this, "mismatched number of type parameters in procedure implementation: {0}",
@@ -2114,57 +2367,56 @@ namespace Microsoft.Boogie MatchFormals(this.OutParams, Proc.OutParams, "out", tc);
}
- foreach (Variable! v in LocVars)
- {
+ foreach (Variable/*!*/ v in LocVars) {
+ Contract.Assert(v != null);
v.Typecheck(tc);
}
IdentifierExprSeq oldFrame = tc.Frame;
tc.Frame = Proc.Modifies;
- foreach (Block b in Blocks)
- {
+ foreach (Block b in Blocks) {
b.Typecheck(tc);
}
- assert tc.Frame == Proc.Modifies;
+ Contract.Assert(tc.Frame == Proc.Modifies);
tc.Frame = oldFrame;
}
- void MatchFormals(VariableSeq! implFormals, VariableSeq! procFormals,
- string! inout, TypecheckingContext! tc)
- {
- if (implFormals.Length != procFormals.Length)
- {
+ void MatchFormals(VariableSeq/*!*/ implFormals, VariableSeq/*!*/ procFormals, string/*!*/ inout, TypecheckingContext/*!*/ tc) {
+ Contract.Requires(implFormals != null);
+ Contract.Requires(procFormals != null);
+ Contract.Requires(inout != null);
+ Contract.Requires(tc != null);
+ if (implFormals.Length != procFormals.Length) {
tc.Error(this, "mismatched number of {0}-parameters in procedure implementation: {1}",
inout, this.Name);
- }
- else
- {
+ } else {
// unify the type parameters so that types can be compared
- assert Proc != null;
- assert this.TypeParameters.Length == Proc.TypeParameters.Length;
-
- IDictionary<TypeVariable!, Type!>! subst1 =
- new Dictionary<TypeVariable!, Type!> ();
- IDictionary<TypeVariable!, Type!>! subst2 =
- new Dictionary<TypeVariable!, Type!> ();
+ Contract.Assert(Proc != null);
+ Contract.Assert(this.TypeParameters.Length == Proc.TypeParameters.Length);
+
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst1 =
+ new Dictionary<TypeVariable/*!*/, Type/*!*/>();
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst2 =
+ new Dictionary<TypeVariable/*!*/, Type/*!*/>();
for (int i = 0; i < this.TypeParameters.Length; ++i) {
- TypeVariable! newVar =
- new TypeVariable (Token.NoToken, Proc.TypeParameters[i].Name);
+ TypeVariable/*!*/ newVar =
+ new TypeVariable(Token.NoToken, Proc.TypeParameters[i].Name);
+ Contract.Assert(newVar != null);
subst1.Add(Proc.TypeParameters[i], newVar);
subst2.Add(this.TypeParameters[i], newVar);
}
- for (int i = 0; i < implFormals.Length; i++)
- {
+ for (int i = 0; i < implFormals.Length; i++) {
// the names of the formals are allowed to change from the proc to the impl
// but types must be identical
- Type t = ((Variable!)implFormals[i]).TypedIdent.Type.Substitute(subst2);
- Type u = ((Variable!)procFormals[i]).TypedIdent.Type.Substitute(subst1);
- if (!t.Equals(u))
- {
- string! a = (!) ((Variable!)implFormals[i]).Name;
- string! b = (!) ((Variable!)procFormals[i]).Name;
- string! c;
+ Type t = cce.NonNull((Variable)implFormals[i]).TypedIdent.Type.Substitute(subst2);
+ Type u = cce.NonNull((Variable)procFormals[i]).TypedIdent.Type.Substitute(subst1);
+ if (!t.Equals(u)) {
+ string/*!*/ a = cce.NonNull((Variable)implFormals[i]).Name;
+ Contract.Assert(a != null);
+ string/*!*/ b = cce.NonNull((Variable)procFormals[i]).Name;
+ Contract.Assert(b != null);
+ string/*!*/ c;
if (a == b) {
c = a;
} else {
@@ -2180,44 +2432,41 @@ namespace Microsoft.Boogie public void ResetImplFormalMap() {
this.formalMap = null;
}
- public Hashtable /*Variable->Expr*/! GetImplFormalMap()
- {
+ public Hashtable /*Variable->Expr*//*!*/ GetImplFormalMap() {
+ Contract.Ensures(Contract.Result<Hashtable>() != null);
+
if (this.formalMap != null)
return this.formalMap;
- else
- {
- Hashtable /*Variable->Expr*/! map = new Hashtable /*Variable->Expr*/ (InParams.Length + OutParams.Length);
+ else {
+ Hashtable /*Variable->Expr*//*!*/ map = new Hashtable /*Variable->Expr*/ (InParams.Length + OutParams.Length);
- assume this.Proc != null;
- assume InParams.Length == Proc.InParams.Length;
- for (int i = 0; i < InParams.Length; i++)
- {
- Variable! v = (!) InParams[i];
+ Contract.Assume(this.Proc != null);
+ Contract.Assume(InParams.Length == Proc.InParams.Length);
+ for (int i = 0; i < InParams.Length; i++) {
+ Variable/*!*/ v = InParams[i];
+ Contract.Assert(v != null);
IdentifierExpr ie = new IdentifierExpr(v.tok, v);
- Variable! pv = (!) Proc.InParams[i];
+ Variable/*!*/ pv = Proc.InParams[i];
+ Contract.Assert(pv != null);
map.Add(pv, ie);
}
System.Diagnostics.Debug.Assert(OutParams.Length == Proc.OutParams.Length);
- for (int i = 0; i < OutParams.Length; i++)
- {
- Variable! v = (!) OutParams[i];
+ for (int i = 0; i < OutParams.Length; i++) {
+ Variable/*!*/ v = cce.NonNull(OutParams[i]);
IdentifierExpr ie = new IdentifierExpr(v.tok, v);
- Variable! pv = (!) Proc.OutParams[i];
+ Variable pv = cce.NonNull(Proc.OutParams[i]);
map.Add(pv, ie);
}
this.formalMap = map;
- if (CommandLineOptions.Clo.PrintWithUniqueASTIds)
- {
+ if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
Console.WriteLine("Implementation.GetImplFormalMap on {0}:", this.Name);
- using (TokenTextWriter stream = new TokenTextWriter("<console>", Console.Out, false))
- {
- foreach (DictionaryEntry e in map)
- {
+ using (TokenTextWriter stream = new TokenTextWriter("<console>", Console.Out, false)) {
+ foreach (DictionaryEntry e in map) {
Console.Write(" ");
- ((Variable!)e.Key).Emit(stream, 0);
+ cce.NonNull((Variable/*!*/)e.Key).Emit(stream, 0);
Console.Write(" --> ");
- ((Expr!)e.Value).Emit(stream);
+ cce.NonNull((Expr)e.Value).Emit(stream);
Console.WriteLine();
}
}
@@ -2230,14 +2479,11 @@ namespace Microsoft.Boogie /// <summary>
/// Instrument the blocks with the inferred invariants
/// </summary>
- public override void InstrumentWithInvariants()
- {
- foreach (Block b in this.Blocks)
- {
- if (b.Lattice != null)
- {
- assert b.PreInvariant != null; /* If the pre-abstract state is null, then something is wrong */
- assert b.PostInvariant != null; /* If the post-state is null, then something is wrong */
+ public override void InstrumentWithInvariants() {
+ foreach (Block b in this.Blocks) {
+ if (b.Lattice != null) {
+ Contract.Assert(b.PreInvariant != null); /* If the pre-abstract state is null, then something is wrong */
+ Contract.Assert(b.PostInvariant != null); /* If the post-state is null, then something is wrong */
bool instrumentEntry;
bool instrumentExit;
@@ -2250,21 +2496,23 @@ namespace Microsoft.Boogie instrumentEntry = b.widenBlock;
instrumentExit = false;
break;
- default:
- assert false; // unexpected InstrumentationPlaces value
+ default: {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // unexpected InstrumentationPlaces value
}
-
+
if (instrumentEntry || instrumentExit) {
CmdSeq newCommands = new CmdSeq();
if (instrumentEntry) {
- Expr inv = (Expr) b.Lattice.ToPredicate(b.PreInvariant); /*b.PreInvariantBuckets.GetDisjunction(b.Lattice);*/
- PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken,inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
+ Expr inv = (Expr)b.Lattice.ToPredicate(b.PreInvariant); /*b.PreInvariantBuckets.GetDisjunction(b.Lattice);*/
+ PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
newCommands.Add(cmd);
}
newCommands.AddRange(b.Cmds);
if (instrumentExit) {
- Expr inv = (Expr) b.Lattice.ToPredicate(b.PostInvariant);
- PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken,inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
+ Expr inv = (Expr)b.Lattice.ToPredicate(b.PostInvariant);
+ PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
newCommands.Add(cmd);
}
b.Cmds = newCommands;
@@ -2277,48 +2525,50 @@ namespace Microsoft.Boogie /// Return a collection of blocks that are reachable from the block passed as a parameter.
/// The block must be defined in the current implementation
/// </summary>
- public ICollection<Block!> GetConnectedComponents(Block! startingBlock)
- {
- assert this.Blocks.Contains(startingBlock);
+ public ICollection<Block/*!*/> GetConnectedComponents(Block startingBlock) {
+ Contract.Requires(startingBlock != null);
+ Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<Block>>(), true));
+ Contract.Assert(this.Blocks.Contains(startingBlock));
- if(!this.BlockPredecessorsComputed)
+ if (!this.BlockPredecessorsComputed)
ComputeStronglyConnectedComponents();
#if DEBUG_PRINT
System.Console.WriteLine("* Strongly connected components * \n{0} \n ** ", scc);
#endif
- foreach(ICollection<Block!> component in (!) this.scc)
- {
- foreach(Block! b in component)
- {
- if(b == startingBlock) // We found the compontent that owns the startingblock
+ foreach (ICollection<Block/*!*/> component in cce.NonNull(this.scc)) {
+ foreach (Block/*!*/ b in component) {
+ Contract.Assert(b != null);
+ if (b == startingBlock) // We found the compontent that owns the startingblock
{
return component;
}
}
}
- assert false; // if we are here, it means that the block is not in one of the components. This is an error.
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // if we are here, it means that the block is not in one of the components. This is an error.
}
/// <summary>
/// Compute the strongly connected compontents of the blocks in the implementation.
/// As a side effect, it also computes the "predecessor" relation for the block in the implementation
/// </summary>
- override public void ComputeStronglyConnectedComponents()
- {
- if(!this.BlockPredecessorsComputed)
- ComputedPredecessorsForBlocks();
+ override public void ComputeStronglyConnectedComponents() {
+ if (!this.BlockPredecessorsComputed)
+ ComputedPredecessorsForBlocks();
- Adjacency<Block!> next = new Adjacency<Block!>(Successors);
- Adjacency<Block!> prev = new Adjacency<Block!>(Predecessors);
+ Adjacency<Block/*!*/> next = new Adjacency<Block/*!*/>(Successors);
+ Adjacency<Block/*!*/> prev = new Adjacency<Block/*!*/>(Predecessors);
- this.scc = new StronglyConnectedComponents<Block!>(this.Blocks, next, prev);
+ this.scc = new StronglyConnectedComponents<Block/*!*/>(this.Blocks, next, prev);
scc.Compute();
- foreach(Block! block in this.Blocks)
- {
+ foreach (Block/*!*/ block in this.Blocks) {
+ Contract.Assert(block != null);
block.Predecessors = new BlockSeq();
}
@@ -2327,10 +2577,9 @@ namespace Microsoft.Boogie /// <summary>
/// Reset the abstract stated computed before
/// </summary>
- override public void ResetAbstractInterpretationState()
- {
- foreach(Block! b in this.Blocks)
- {
+ override public void ResetAbstractInterpretationState() {
+ foreach (Block/*!*/ b in this.Blocks) {
+ Contract.Assert(b != null);
b.ResetAbstractInterpretationState();
}
}
@@ -2339,21 +2588,20 @@ namespace Microsoft.Boogie /// A private method used as delegate for the strongly connected components.
/// It return, given a node, the set of its successors
/// </summary>
- private IEnumerable/*<Block!>*/! Successors(Block! node)
- {
+ private IEnumerable/*<Block!>*//*!*/ Successors(Block node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<IEnumerable>() != null);
+
GotoCmd gotoCmd = node.TransferCmd as GotoCmd;
- if(gotoCmd != null)
- { // If it is a gotoCmd
- assert gotoCmd.labelTargets != null;
+ if (gotoCmd != null) { // If it is a gotoCmd
+ Contract.Assert(gotoCmd.labelTargets != null);
return gotoCmd.labelTargets;
- }
- else
- { // otherwise must be a ReturnCmd
- assert node.TransferCmd is ReturnCmd;
+ } else { // otherwise must be a ReturnCmd
+ Contract.Assert(node.TransferCmd is ReturnCmd);
- return new List<Block!>();
+ return new List<Block/*!*/>();
}
}
@@ -2361,26 +2609,25 @@ namespace Microsoft.Boogie /// A private method used as delegate for the strongly connected components.
/// It return, given a node, the set of its predecessors
/// </summary>
- private IEnumerable/*<Block!>*/! Predecessors(Block! node)
- {
- assert this.BlockPredecessorsComputed;
+ private IEnumerable/*<Block!>*//*!*/ Predecessors(Block node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<IEnumerable>() != null);
+
+ Contract.Assert(this.BlockPredecessorsComputed);
- return node.Predecessors;
+ return node.Predecessors;
}
/// <summary>
/// Compute the predecessor informations for the blocks
/// </summary>
- private void ComputedPredecessorsForBlocks()
- {
- foreach (Block b in this.Blocks)
- {
+ private void ComputedPredecessorsForBlocks() {
+ foreach (Block b in this.Blocks) {
GotoCmd gtc = b.TransferCmd as GotoCmd;
- if (gtc != null)
- {
- assert gtc.labelTargets != null;
- foreach (Block! dest in gtc.labelTargets)
- {
+ if (gtc != null) {
+ Contract.Assert(gtc.labelTargets != null);
+ foreach (Block/*!*/ dest in gtc.labelTargets) {
+ Contract.Assert(dest != null);
dest.Predecessors.Add(b);
}
}
@@ -2390,64 +2637,78 @@ namespace Microsoft.Boogie public void PruneUnreachableBlocks() {
ArrayList /*Block!*/ visitNext = new ArrayList /*Block!*/ ();
- List<Block!> reachableBlocks = new List<Block!>();
+ List<Block/*!*/> reachableBlocks = new List<Block/*!*/>();
System.Compiler.IMutableSet /*Block!*/ reachable = new System.Compiler.HashSet /*Block!*/ (); // the set of elements in "reachableBlocks"
visitNext.Add(this.Blocks[0]);
while (visitNext.Count != 0) {
- Block! b = (Block!)visitNext[visitNext.Count-1];
- visitNext.RemoveAt(visitNext.Count-1);
+ Block b = cce.NonNull((Block)visitNext[visitNext.Count - 1]);
+ visitNext.RemoveAt(visitNext.Count - 1);
if (!reachable.Contains(b)) {
- reachableBlocks.Add(b);
- reachable.Add(b);
- if (b.TransferCmd is GotoCmd) {
- foreach (Cmd! s in b.Cmds) {
- if (s is PredicateCmd) {
- LiteralExpr e = ((PredicateCmd)s).Expr as LiteralExpr;
- if (e != null && e.IsFalse) {
- // This statement sequence will never reach the end, because of this "assume false" or "assert false".
- // Hence, it does not reach its successors.
- b.TransferCmd = new ReturnCmd(b.TransferCmd.tok);
- goto NEXT_BLOCK;
- }
- }
- }
- // it seems that the goto statement at the end may be reached
- foreach (Block! succ in (!)((GotoCmd)b.TransferCmd).labelTargets) {
- visitNext.Add(succ);
+ reachableBlocks.Add(b);
+ reachable.Add(b);
+ if (b.TransferCmd is GotoCmd) {
+ foreach (Cmd/*!*/ s in b.Cmds) {
+ Contract.Assert(s != null);
+ if (s is PredicateCmd) {
+ LiteralExpr e = ((PredicateCmd)s).Expr as LiteralExpr;
+ if (e != null && e.IsFalse) {
+ // This statement sequence will never reach the end, because of this "assume false" or "assert false".
+ // Hence, it does not reach its successors.
+ b.TransferCmd = new ReturnCmd(b.TransferCmd.tok);
+ goto NEXT_BLOCK;
}
+ }
+ }
+ // it seems that the goto statement at the end may be reached
+ foreach (Block succ in cce.NonNull((GotoCmd)b.TransferCmd).labelTargets) {
+ Contract.Assume(succ != null);
+ visitNext.Add(succ);
}
+ }
+ }
+ NEXT_BLOCK: {
}
- NEXT_BLOCK: {}
}
this.Blocks = reachableBlocks;
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitImplementation(this);
}
}
- public class TypedIdent : Absy
- {
+ public class TypedIdent : Absy {
public const string NoName = "";
- public string! Name;
- public Type! Type;
+ public string/*!*/ Name;
+ public Type/*!*/ Type;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Name != null);
+ Contract.Invariant(Type != null);
+ }
+
public Expr WhereExpr;
- // [NotDelayed]
- public TypedIdent (IToken! tok, string! name, Type! type)
- ensures this.WhereExpr == null; //PM: needed to verify BoogiePropFactory.FreshBoundVariable
- {
- this(tok, name, type, null); // here for aesthetic reasons
+ // [NotDelayed]
+ public TypedIdent(IToken/*!*/ tok, string/*!*/ name, Type/*!*/ type)
+ : this(tok, name, type, null) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Contract.Requires(type != null);
+ Contract.Ensures(this.WhereExpr == null); //PM: needed to verify BoogiePropFactory.FreshBoundVariable
+ //:this(tok, name, type, null); // here for aesthetic reasons
}
// [NotDelayed]
- public TypedIdent (IToken! tok, string! name, Type! type, Expr whereExpr)
- : base(tok)
- ensures this.WhereExpr == whereExpr;
- {
+ public TypedIdent(IToken/*!*/ tok, string/*!*/ name, Type/*!*/ type, Expr whereExpr)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Contract.Requires(type != null);
+ Contract.Ensures(this.WhereExpr == whereExpr);
this.Name = name;
this.Type = type;
this.WhereExpr = whereExpr;
@@ -2458,43 +2719,41 @@ namespace Microsoft.Boogie return this.Name != NoName;
}
}
- public void Emit(TokenTextWriter! stream)
- {
+ public void Emit(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
stream.SetToken(this);
- if (this.Name != NoName)
- {
+ if (this.Name != NoName) {
stream.Write("{0}: ", TokenTextWriter.SanitizeIdentifier(this.Name));
}
this.Type.Emit(stream);
- if (this.WhereExpr != null)
- {
+ if (this.WhereExpr != null) {
stream.Write(" where ");
this.WhereExpr.Emit(stream);
}
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
// NOTE: WhereExpr needs to be resolved by the caller, because the caller must provide a modified ResolutionContext
this.Type = this.Type.ResolveType(rc);
}
- public override void Typecheck(TypecheckingContext! tc)
- {
-// type variables can occur when working with polymorphic functions/procedures
-// if (!this.Type.IsClosed)
-// tc.Error(this, "free variables in type of an identifier: {0}",
-// this.Type.FreeVariables);
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ // type variables can occur when working with polymorphic functions/procedures
+ // if (!this.Type.IsClosed)
+ // tc.Error(this, "free variables in type of an identifier: {0}",
+ // this.Type.FreeVariables);
if (this.WhereExpr != null) {
this.WhereExpr.Typecheck(tc);
- assert this.WhereExpr.Type != null; // follows from postcondition of Expr.Typecheck
- if (!this.WhereExpr.Type.Unify(Type.Bool))
- {
+ Contract.Assert(this.WhereExpr.Type != null); // follows from postcondition of Expr.Typecheck
+ if (!this.WhereExpr.Type.Unify(Type.Bool)) {
tc.Error(this, "where clauses must be of type bool");
}
}
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitTypedIdent(this);
}
}
@@ -2513,26 +2772,18 @@ namespace Microsoft.Boogie /// The right-hand value of the setter is not allowed to be null; that is,
/// null can occur in the list only as an "unused" element.
/// </summary>
- public class LatticeElementList : ArrayList
- {
- public new /*Maybe null*/ AI.Lattice.Element this [ int i ]
- {
- get
- {
- if (i < Count)
- {
+ public class LatticeElementList : ArrayList {
+ public new /*Maybe null*/ AI.Lattice.Element this[int i] {
+ get {
+ if (i < Count) {
return (AI.Lattice.Element)base[i];
- }
- else
- {
+ } else {
return null;
}
}
- set
- {
+ set {
System.Diagnostics.Debug.Assert(value != null);
- while (Count <= i)
- {
+ while (Count <= i) {
Add(null);
}
base[i] = value;
@@ -2546,60 +2797,51 @@ namespace Microsoft.Boogie /// </summary>
/// <param name="lattice"></param>
/// <returns></returns>
- public Expr GetDisjunction(AI.Lattice! lattice)
- {
+ public Expr GetDisjunction(AI.Lattice lattice) {
+ Contract.Requires(lattice != null);
Expr disjunction = null;
- foreach (AI.Lattice.Element el in this)
- {
- if (el != null)
- {
- Expr e = (Expr) lattice.ToPredicate(el);
- if (disjunction == null)
- {
+ foreach (AI.Lattice.Element el in this) {
+ if (el != null) {
+ Expr e = (Expr)lattice.ToPredicate(el);
+ if (disjunction == null) {
disjunction = e;
- }
- else
- {
+ } else {
disjunction = Expr.Or(disjunction, e);
}
}
}
- if (disjunction == null)
- {
+ if (disjunction == null) {
return Expr.False;
- }
- else
- {
+ } else {
return disjunction;
}
}
}
-
-
public abstract class BoogieFactory {
- public static Expr! IExpr2Expr(AI.IExpr! e) {
+ public static Expr IExpr2Expr(AI.IExpr e) {
+ Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
Variable v = e as Variable;
if (v != null) {
return new IdentifierExpr(Token.NoToken, v);
- }
- else if (e is AI.IVariable) { // but not a Variable
+ } else if (e is AI.IVariable) { // but not a Variable
return new AIVariableExpr(Token.NoToken, (AI.IVariable)e);
- }
- else if (e is IdentifierExpr.ConstantFunApp) {
+ } else if (e is IdentifierExpr.ConstantFunApp) {
return ((IdentifierExpr.ConstantFunApp)e).IdentifierExpr;
- }
- else if (e is QuantifierExpr.AIQuantifier) {
+ } else if (e is QuantifierExpr.AIQuantifier) {
return ((QuantifierExpr.AIQuantifier)e).arg.RealQuantifier;
- }
- else {
+ } else {
return (Expr)e;
}
}
- public static ExprSeq! IExprArray2ExprSeq(IList/*<AI.IExpr!>*/! a) {
+ public static ExprSeq IExprArray2ExprSeq(IList/*<AI.IExpr!>*/ a) {
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExprSeq>() != null);
Expr[] e = new Expr[a.Count];
int i = 0;
- foreach (AI.IExpr! aei in a) {
+ foreach (AI.IExpr/*!*/ aei in a) {
+ Contract.Assert(aei != null);
e[i] = IExpr2Expr(aei);
i++;
}
@@ -2608,15 +2850,16 @@ namespace Microsoft.Boogie // Convert a Boogie type into an AIType if possible. This should be
// extended when AIFramework gets more types.
- public static AI.AIType! Type2AIType(Type! t)
- {
-// if (t.IsRef)
-// return AI.Ref.Type;
-// else
+ public static AI.AIType Type2AIType(Type t) {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result<AI.AIType>() != null);
+ // if (t.IsRef)
+ // return AI.Ref.Type;
+ // else
if (t.IsInt)
return AI.Int.Type;
-// else if (t.IsName) PR: how to handle this case?
-// return AI.FieldName.Type;
+ // else if (t.IsName) PR: how to handle this case?
+ // return AI.FieldName.Type;
else
return AI.Value.Type;
}
@@ -2627,125 +2870,129 @@ namespace Microsoft.Boogie // Generic Sequences
//---------------------------------------------------------------------
- public sealed class TypedIdentSeq : PureCollections.Sequence
- {
- public TypedIdentSeq(params Type[]! args) : base(args) { }
- public new TypedIdent this[int index]
- {
- get
- {
+ public sealed class TypedIdentSeq : PureCollections.Sequence {
+ public TypedIdentSeq(params Type[]/*!*/ args)
+ : base(args) {
+ Contract.Requires(args != null);
+ }
+ public new TypedIdent this[int index] {
+ get {
return (TypedIdent)base[index];
}
- set
- {
+ set {
base[index] = value;
}
}
}
- public sealed class RequiresSeq : PureCollections.Sequence
- {
- public RequiresSeq(params Requires[]! args) : base(args) { }
- public new Requires! this[int index]
- {
- get
- {
- return (Requires!) base[index];
+ public sealed class RequiresSeq : PureCollections.Sequence {
+ public RequiresSeq(params Requires[]/*!*/ args)
+ : base(args) {
+ Contract.Requires(args != null);
+ }
+ public new Requires/*!*/ this[int index] {
+ get {
+ Contract.Ensures(Contract.Result<Requires>() != null);
+
+ return cce.NonNull((Requires/*!*/)base[index]);
}
- set
- {
+ set {
base[index] = value;
}
}
}
- public sealed class EnsuresSeq : PureCollections.Sequence
- {
- public EnsuresSeq(params Ensures[]! args) : base(args) { }
- public new Ensures! this[int index]
- {
- get
- {
- return (Ensures!) base[index];
+ public sealed class EnsuresSeq : PureCollections.Sequence {
+ public EnsuresSeq(params Ensures[]/*!*/ args)
+ : base(args) {
+ Contract.Requires(args != null);
+ }
+ public new Ensures/*!*/ this[int index] {
+ get {
+ Contract.Ensures(Contract.Result<Ensures>() != null);
+ return cce.NonNull((Ensures/*!*/)base[index]);
}
- set
- {
+ set {
base[index] = value;
}
}
}
- public sealed class VariableSeq : PureCollections.Sequence
- {
- public VariableSeq(params Variable[]! args)
- : base(args)
- {
+ public sealed class VariableSeq : PureCollections.Sequence {
+ public VariableSeq(params Variable[]/*!*/ args)
+ : base(args) {
+ Contract.Requires(args != null);
}
- public VariableSeq(VariableSeq! varSeq)
- : base(varSeq)
- {
+ public VariableSeq(VariableSeq/*!*/ varSeq)
+ : base(varSeq) {
+ Contract.Requires(varSeq != null);
}
- public new Variable this[int index]
- {
- get
- {
+ public new Variable this[int index] {
+ get {
return (Variable)base[index];
}
- set
- {
+ set {
base[index] = value;
}
}
- public void Emit(TokenTextWriter! stream)
- {
+ public void Emit(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
string sep = "";
- foreach (Variable! v in this)
- {
+ foreach (Variable/*!*/ v in this) {
+ Contract.Assert(v != null);
stream.Write(sep);
sep = ", ";
v.EmitVitals(stream, 0);
}
}
- public TypeSeq! ToTypeSeq { get {
- TypeSeq! res = new TypeSeq ();
- foreach(Variable! v in this)
- res.Add(v.TypedIdent.Type);
- return res;
- } }
+ public TypeSeq/*!*/ ToTypeSeq {
+ get {
+ Contract.Ensures(Contract.Result<TypeSeq>() != null);
+
+ TypeSeq/*!*/ res = new TypeSeq();
+ foreach (Variable/*!*/ v in this) {
+ Contract.Assert(v != null);
+ res.Add(v.TypedIdent.Type);
+ }
+ return res;
+ }
+ }
}
- public sealed class TypeSeq : PureCollections.Sequence
- {
- public TypeSeq(params Type[]! args)
- : base(args)
- {
+ public sealed class TypeSeq : PureCollections.Sequence {
+ public TypeSeq(params Type[]/*!*/ args)
+ : base(args) {
+ Contract.Requires(args != null);
}
- public TypeSeq(TypeSeq! varSeq)
- : base(varSeq)
- {
+ public TypeSeq(TypeSeq/*!*/ varSeq)
+ : base(varSeq) {
+ Contract.Requires(varSeq != null);
}
- public new Type! this[int index]
- {
- get
- {
- return (Type!)base[index];
+ public new Type/*!*/ this[int index] {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ return cce.NonNull((Type/*!*/)base[index]);
}
- set
- {
+ set {
base[index] = value;
}
}
- public List<Type!>! ToList() {
- List<Type!>! res = new List<Type!> (Length);
- foreach (Type! t in this)
+ public List<Type/*!*/>/*!*/ ToList() {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
+ List<Type/*!*/>/*!*/ res = new List<Type/*!*/>(Length);
+ foreach (Type/*!*/ t in this) {
+ Contract.Assert(t != null);
res.Add(t);
+ }
return res;
}
- public void Emit(TokenTextWriter! stream, string! separator)
- {
+ public void Emit(TokenTextWriter stream, string separator) {
+ Contract.Requires(separator != null);
+ Contract.Requires(stream != null);
string sep = "";
- foreach (Type! v in this)
- {
+ foreach (Type/*!*/ v in this) {
+ Contract.Assert(v != null);
stream.Write(sep);
sep = separator;
v.Emit(stream);
@@ -2753,94 +3000,100 @@ namespace Microsoft.Boogie }
}
- public sealed class TypeVariableSeq : PureCollections.Sequence
- {
- public TypeVariableSeq(params TypeVariable[]! args)
- : base(args)
- {
- }
- public TypeVariableSeq(TypeVariableSeq! varSeq)
- : base(varSeq)
- {
- }
-/* PR: the following two constructors cause Spec# crashes
- public TypeVariableSeq(TypeVariable! var)
- : base(new TypeVariable! [] { var })
- {
- }
- public TypeVariableSeq()
- : base(new TypeVariable![0])
- {
- } */
- public new TypeVariable! this[int index]
- {
- get
- {
- return (TypeVariable!)base[index];
+ public sealed class TypeVariableSeq : PureCollections.Sequence {
+ public TypeVariableSeq(params TypeVariable[]/*!*/ args)
+ : base(args) {
+ Contract.Requires(args != null);
+ }
+ public TypeVariableSeq(TypeVariableSeq/*!*/ varSeq)
+ : base(varSeq) {
+ Contract.Requires(varSeq != null);
+ }
+ /* PR: the following two constructors cause Spec# crashes
+ public TypeVariableSeq(TypeVariable! var)
+ : base(new TypeVariable! [] { var })
+ {
+ }
+ public TypeVariableSeq()
+ : base(new TypeVariable![0])
+ {
+ } */
+ public new TypeVariable/*!*/ this[int index] {
+ get {
+ Contract.Ensures(Contract.Result<TypeVariable>() != null);
+
+ return cce.NonNull((TypeVariable)base[index]);
}
- set
- {
+ set {
base[index] = value;
}
}
- public void AppendWithoutDups(TypeVariableSeq! s1) {
+ public void AppendWithoutDups(TypeVariableSeq s1) {
+ Contract.Requires(s1 != null);
for (int i = 0; i < s1.card; i++) {
- TypeVariable! next = s1[i];
- if (!this.Has(next)) this.Add(next);
+ TypeVariable/*!*/ next = s1[i];
+ Contract.Assert(next != null);
+ if (!this.Has(next))
+ this.Add(next);
}
}
- public void Emit(TokenTextWriter! stream, string! separator)
- {
+ public void Emit(TokenTextWriter stream, string separator) {
+ Contract.Requires(separator != null);
+ Contract.Requires(stream != null);
string sep = "";
- foreach (TypeVariable! v in this)
- {
+ foreach (TypeVariable/*!*/ v in this) {
+ Contract.Assert(v != null);
stream.Write(sep);
sep = separator;
v.Emit(stream);
}
}
- public new TypeVariable[]! ToArray() {
- TypeVariable[]! n = new TypeVariable[Length];
+ public new TypeVariable[] ToArray() {
+ Contract.Ensures(Contract.Result<TypeVariable[]>() != null);
+ TypeVariable[]/*!*/ n = new TypeVariable[Length];
int ct = 0;
- foreach (TypeVariable! var in this)
+ foreach (TypeVariable/*!*/ var in this) {
+ Contract.Assert(var != null);
n[ct++] = var;
+ }
return n;
}
- public List<TypeVariable!>! ToList() {
- List<TypeVariable!>! res = new List<TypeVariable!> (Length);
- foreach (TypeVariable! var in this)
+ public List<TypeVariable/*!*/>/*!*/ ToList() {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));
+ List<TypeVariable/*!*/>/*!*/ res = new List<TypeVariable/*!*/>(Length);
+ foreach (TypeVariable/*!*/ var in this) {
+ Contract.Assert(var != null);
res.Add(var);
+ }
return res;
}
}
- public sealed class IdentifierExprSeq : PureCollections.Sequence
- {
- public IdentifierExprSeq(params IdentifierExpr[]! args)
- : base(args)
- {
+ public sealed class IdentifierExprSeq : PureCollections.Sequence {
+ public IdentifierExprSeq(params IdentifierExpr[]/*!*/ args)
+ : base(args) {
+ Contract.Requires(args != null);
}
- public IdentifierExprSeq(IdentifierExprSeq! ideSeq)
- : base(ideSeq)
- {
+ public IdentifierExprSeq(IdentifierExprSeq/*!*/ ideSeq)
+ : base(ideSeq) {
+ Contract.Requires(ideSeq != null);
}
- public new IdentifierExpr! this[int index]
- {
- get
- {
- return (IdentifierExpr!)base[index];
+ public new IdentifierExpr/*!*/ this[int index] {
+ get {
+ Contract.Ensures(Contract.Result<IdentifierExpr>() != null);
+
+ return cce.NonNull((IdentifierExpr)base[index]);
}
- set
- {
- base[index] = value;
+ set {
+ base[index] = value;
}
}
- public void Emit(TokenTextWriter! stream, bool printWhereComments)
- {
+ public void Emit(TokenTextWriter stream, bool printWhereComments) {
+ Contract.Requires(stream != null);
string sep = "";
- foreach (IdentifierExpr! e in this)
- {
+ foreach (IdentifierExpr/*!*/ e in this) {
+ Contract.Assert(e != null);
stream.Write(sep);
sep = ", ";
e.Emit(stream);
@@ -2855,123 +3108,122 @@ namespace Microsoft.Boogie }
- public sealed class CmdSeq : PureCollections.Sequence
- {
- public CmdSeq(params Cmd[]! args) : base(args){}
- public CmdSeq(CmdSeq! cmdSeq)
- : base(cmdSeq)
- {
- }
- public new Cmd! this[int index]
- {
- get
- {
- return (Cmd!)base[index];
+ public sealed class CmdSeq : PureCollections.Sequence {
+ public CmdSeq(params Cmd[]/*!*/ args)
+ : base(args) {
+ Contract.Requires(args != null);
+ }
+ public CmdSeq(CmdSeq/*!*/ cmdSeq)
+ : base(cmdSeq) {
+ Contract.Requires(cmdSeq != null);
+ }
+ public new Cmd/*!*/ this[int index] {
+ get {
+ Contract.Ensures(Contract.Result<Cmd>() != null);
+
+ return cce.NonNull((Cmd)base[index]);
}
- set
- {
+ set {
base[index] = value;
}
}
}
- public sealed class ExprSeq : PureCollections.Sequence
- {
- public ExprSeq(params Expr[]! args)
- : base(args)
- {
+ public sealed class ExprSeq : PureCollections.Sequence {
+ public ExprSeq(params Expr[]/*!*/ args)
+ : base(args) {
+ Contract.Requires(args != null);
}
- public ExprSeq(ExprSeq! exprSeq)
- : base(exprSeq)
- {
+ public ExprSeq(ExprSeq/*!*/ exprSeq)
+ : base(exprSeq) {
+ Contract.Requires(exprSeq != null);
}
- public new Expr this[int index]
- {
- get
- {
+ public new Expr this[int index] {
+ get {
return (Expr)base[index];
}
- set
- {
+ set {
base[index] = value;
}
}
-
- public new Expr Last() { return (Expr)base.Last(); }
- public static ExprSeq operator +(ExprSeq a, ExprSeq b)
- {
- if (a==null) throw new ArgumentNullException("a");
- if (b==null) throw new ArgumentNullException("b");
- return Append(a,b);
+ public new Expr Last() {
+ return (Expr)base.Last();
}
- public static ExprSeq Append(ExprSeq! s, ExprSeq! t)
- {
- Expr[] n = new Expr[s.card+t.card];
- for (int i = 0; i< s.card; i++) n[i] = s[i];
- for (int i = 0; i< t.card; i++) n[s.card+i] = t[i];
+ public static ExprSeq operator +(ExprSeq a, ExprSeq b) {
+ if (a == null)
+ throw new ArgumentNullException("a");
+ if (b == null)
+ throw new ArgumentNullException("b");
+ return Append(a, b);
+ }
+
+ public static ExprSeq Append(ExprSeq s, ExprSeq t) {
+ Contract.Requires(t != null);
+ Contract.Requires(s != null);
+ Expr[] n = new Expr[s.card + t.card];
+ for (int i = 0; i < s.card; i++)
+ n[i] = s[i];
+ for (int i = 0; i < t.card; i++)
+ n[s.card + i] = t[i];
return new ExprSeq(n);
}
- public void Emit(TokenTextWriter! stream)
- {
+ public void Emit(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
string sep = "";
- foreach (Expr! e in this)
- {
+ foreach (Expr/*!*/ e in this) {
+ Contract.Assert(e != null);
stream.Write(sep);
sep = ", ";
e.Emit(stream);
}
}
- public TypeSeq! ToTypeSeq { get {
- TypeSeq! res = new TypeSeq ();
- foreach(Expr e in this)
- res.Add(((!)e).Type);
- return res;
- } }
+ public TypeSeq/*!*/ ToTypeSeq {
+ get {
+ Contract.Ensures(Contract.Result<TypeSeq>() != null);
+
+ TypeSeq res = new TypeSeq();
+ foreach (Expr e in this)
+ res.Add(cce.NonNull(e).Type);
+ return res;
+ }
+ }
}
- public sealed class TokenSeq : PureCollections.Sequence
- {
- public TokenSeq(params Token[]! args)
- : base(args)
- {
+ public sealed class TokenSeq : PureCollections.Sequence {
+ public TokenSeq(params Token[]/*!*/ args)
+ : base(args) {
+ Contract.Requires(args != null);
}
- public new Token this[int index]
- {
- get
- {
+ public new Token this[int index] {
+ get {
return (Token)base[index];
}
- set
- {
+ set {
base[index] = value;
}
}
}
- public sealed class StringSeq : PureCollections.Sequence
- {
- public StringSeq(params string[]! args)
- : base(args)
- {
+ public sealed class StringSeq : PureCollections.Sequence {
+ public StringSeq(params string[]/*!*/ args)
+ : base(args) {
+ Contract.Requires(args != null);
}
- public new String this[int index]
- {
- get
- {
+ public new String this[int index] {
+ get {
return (String)base[index];
}
- set
- {
+ set {
base[index] = value;
}
}
- public void Emit(TokenTextWriter! stream)
- {
+ public void Emit(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
string sep = "";
- foreach (string! s in this)
- {
+ foreach (string/*!*/ s in this) {
+ Contract.Assert(s != null);
stream.Write(sep);
sep = ", ";
stream.Write(s);
@@ -2979,87 +3231,73 @@ namespace Microsoft.Boogie }
}
- public sealed class BlockSeq : PureCollections.Sequence
- {
- public BlockSeq(params Block[]! args)
- : base(args)
- {
+ public sealed class BlockSeq : PureCollections.Sequence {
+ public BlockSeq(params Block[]/*!*/ args)
+ : base(args) {
+ Contract.Requires(args != null);
}
- public BlockSeq(BlockSeq! blockSeq)
- : base(blockSeq)
- {
+ public BlockSeq(BlockSeq blockSeq)
+ : base(blockSeq) {
+ Contract.Requires(blockSeq != null);
}
- public new Block this[int index]
- {
- get
- {
+ public new Block this[int index] {
+ get {
return (Block)base[index];
}
- set
- {
+ set {
base[index] = value;
}
}
}
public static class Emitter {
- public static void Declarations(List<Declaration!>! decls, TokenTextWriter! stream)
- {
+ public static void Declarations(List<Declaration/*!*/>/*!*/ decls, TokenTextWriter stream) {
+ Contract.Requires(stream != null);
+ Contract.Requires(cce.NonNullElements(decls));
bool first = true;
- foreach (Declaration d in decls)
- {
- if (d == null) continue;
- if (first)
- {
+ foreach (Declaration d in decls) {
+ if (d == null)
+ continue;
+ if (first) {
first = false;
- }
- else
- {
+ } else {
stream.WriteLine();
}
d.Emit(stream, 0);
}
}
}
- public sealed class DeclarationSeq : PureCollections.Sequence
- {
- public DeclarationSeq(params string[]! args)
- : base(args)
- {
+ public sealed class DeclarationSeq : PureCollections.Sequence {
+ public DeclarationSeq(params string[] args)
+ : base(args) {
+ Contract.Requires(args != null);
}
- public new Declaration this[int index]
- {
- get
- {
+ public new Declaration this[int index] {
+ get {
return (Declaration)base[index];
}
- set
- {
+ set {
base[index] = value;
}
}
- public void Emit(TokenTextWriter! stream)
- {
+ public void Emit(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
bool first = true;
- foreach (Declaration d in this)
- {
- if (d == null) continue;
- if (first)
- {
+ foreach (Declaration d in this) {
+ if (d == null)
+ continue;
+ if (first) {
first = false;
- }
- else
- {
+ } else {
stream.WriteLine();
}
d.Emit(stream, 0);
}
}
- public void InstrumentWithInvariants ()
- {
- foreach (Declaration! d in this)
- {
+ public void InstrumentWithInvariants() {
+ foreach (Declaration/*!*/ d in this) {
+ Contract.Assert(d != null);
d.InstrumentWithInvariants();
}
}
@@ -3069,24 +3307,20 @@ namespace Microsoft.Boogie #region Regular Expressions
// a data structure to recover the "program structure" from the flow graph
- public sealed class RESeq : PureCollections.Sequence
- {
- public RESeq(params RE[]! args)
- : base (args)
- {
+ public sealed class RESeq : PureCollections.Sequence {
+ public RESeq(params RE[] args)
+ : base(args) {
+ Contract.Requires(args != null);
}
- public RESeq(RESeq! reSeq)
- : base(reSeq)
- {
+ public RESeq(RESeq reSeq)
+ : base(reSeq) {
+ Contract.Requires(reSeq != null);
}
- public new RE this[int index]
- {
- get
- {
+ public new RE this[int index] {
+ get {
return (RE)base[index];
}
- set
- {
+ set {
base[index] = value;
}
}
@@ -3101,119 +3335,140 @@ namespace Microsoft.Boogie // }
// }
}
- public abstract class RE : Cmd
- {
- public RE() : base(Token.NoToken) {}
- public override void AddAssignedVariables(VariableSeq! vars) { throw new NotImplementedException(); }
+ public abstract class RE : Cmd {
+ public RE()
+ : base(Token.NoToken) {
+ }
+ public override void AddAssignedVariables(VariableSeq vars) {
+ //Contract.Requires(vars != null);
+ throw new NotImplementedException();
+ }
}
- public class AtomicRE : RE
- {
- public Block! b;
- public AtomicRE(Block! block) { b = block; }
- public override void Resolve(ResolutionContext! rc)
- {
+ public class AtomicRE : RE {
+ public Block/*!*/ b;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(b != null);
+ }
+
+ public AtomicRE(Block block) {
+ Contract.Requires(block != null);
+ b = block;
+ }
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
b.Resolve(rc);
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
b.Typecheck(tc);
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
- b.Emit(stream,level);
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
+ b.Emit(stream, 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.VisitAtomicRE(this);
}
}
- public abstract class CompoundRE : RE
- {
- public override void Resolve(ResolutionContext! rc)
- {
+ public abstract class CompoundRE : RE {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
return;
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
return;
}
}
- public class Sequential : CompoundRE
- {
- public RE! first;
- public RE! second;
- public Sequential(RE! a, RE! b)
- {
+ public class Sequential : CompoundRE {
+ public RE/*!*/ first;
+ public RE/*!*/ second;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(first != null);
+ Contract.Invariant(second != null);
+ }
+
+ public Sequential(RE a, RE b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
first = a;
second = b;
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
stream.WriteLine();
stream.WriteLine("{0};", Indent(level));
- first.Emit(stream,level+1);
- second.Emit(stream,level+1);
+ first.Emit(stream, level + 1);
+ second.Emit(stream, level + 1);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitSequential(this);
}
}
- public class Choice : CompoundRE
- {
- public RESeq! rs;
- public Choice(RESeq! operands)
- {
+ public class Choice : CompoundRE {
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(rs != null);
+ }
+
+ public RESeq/*!*/ rs;
+ public Choice(RESeq operands) {
+ Contract.Requires(operands != null);
rs = operands;
// base();
}
- public override void Emit(TokenTextWriter! stream, int level)
- {
+ public override void Emit(TokenTextWriter stream, int level) {
+ //Contract.Requires(stream != null);
stream.WriteLine();
stream.WriteLine("{0}[]", Indent(level));
- foreach (RE! r in rs )
- r.Emit(stream,level+1);
+ foreach (RE/*!*/ r in rs) {
+ Contract.Assert(r != null);
+ r.Emit(stream, level + 1);
+ }
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitChoice(this);
}
}
- public class DAG2RE
- {
- public static RE! Transform(Block! b)
- {
+ public class DAG2RE {
+ public static RE Transform(Block b) {
+ Contract.Requires(b != null);
+ Contract.Ensures(Contract.Result<RE>() != null);
TransferCmd tc = b.TransferCmd;
- if ( tc is ReturnCmd )
- {
+ if (tc is ReturnCmd) {
return new AtomicRE(b);
- }
- else if ( tc is GotoCmd )
- {
- GotoCmd! g = (GotoCmd) tc ;
- assume g.labelTargets != null;
- if ( g.labelTargets.Length == 1 )
- {
- return new Sequential(new AtomicRE(b),Transform( (!) g.labelTargets[0]));
- }
- else
- {
+ } else if (tc is GotoCmd) {
+ GotoCmd/*!*/ g = (GotoCmd)tc;
+ Contract.Assert(g != null);
+ Contract.Assume(g.labelTargets != null);
+ if (g.labelTargets.Length == 1) {
+ return new Sequential(new AtomicRE(b), Transform(cce.NonNull(g.labelTargets[0])));
+ } else {
RESeq rs = new RESeq();
- foreach (Block! target in g.labelTargets )
- {
+ foreach (Block/*!*/ target in g.labelTargets) {
+ Contract.Assert(target != null);
RE r = Transform(target);
rs.Add(r);
}
RE second = new Choice(rs);
- return new Sequential(new AtomicRE(b),second);
+ return new Sequential(new AtomicRE(b), second);
+ }
+ } else {
+ {
+ Contract.Assume(false);
+ throw new cce.UnreachableException();
}
- }
- else
- {
- assume false;
return new AtomicRE(b);
}
}
@@ -3224,21 +3479,29 @@ namespace Microsoft.Boogie // NOTE: This class is here for convenience, since this file's
// classes are used pretty much everywhere.
- public class BoogieDebug
- {
+ public class BoogieDebug {
public static bool DoPrinting = false;
- public static void Write (string! format, params object[]! args)
- {
- if (DoPrinting) { Console.Error.Write(format, args); }
+ public static void Write(string format, params object[] args) {
+ Contract.Requires(args != null);
+ Contract.Requires(format != null);
+ if (DoPrinting) {
+ Console.Error.Write(format, args);
+ }
}
- public static void WriteLine (string! format, params object[]! args)
- {
- if (DoPrinting) { Console.Error.WriteLine(format, args); }
+ public static void WriteLine(string format, params object[] args) {
+ Contract.Requires(args != null);
+ Contract.Requires(format != null);
+ if (DoPrinting) {
+ Console.Error.WriteLine(format, args);
+ }
}
- public static void WriteLine () { if (DoPrinting) { Console.Error.WriteLine(); } }
+ public static void WriteLine() {
+ if (DoPrinting) {
+ Console.Error.WriteLine();
+ }
+ }
}
-
-}
+}
\ No newline at end of file |