From 8567d68f7f04f87b2d4270e18713bdcdf4d26031 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 10 Feb 2014 18:14:46 -0800 Subject: Fixed errors in the use of Code Contracts --- Source/AbsInt/IntervalDomain.cs | 1 + Source/Core/Absy.cs | 2 +- Source/Core/AbsyQuant.cs | 1 + Source/Core/DeadVarElim.cs | 39 ++++++++++++++++++--------------------- Source/Core/Duplicator.cs | 6 +++--- Source/Houdini/Houdini.cs | 4 ---- Source/VCGeneration/VC.cs | 2 +- 7 files changed, 25 insertions(+), 30 deletions(-) (limited to 'Source') diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 0e095c44..0dbcaaba 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -39,6 +39,7 @@ namespace Microsoft.Boogie.AbstractInterpretation public readonly BigInteger? Lo; public readonly BigInteger? Hi; public Node Next; // always sorted according to StrictlyBefore; readonly after full initialization + [Pure] public static bool StrictlyBefore(Variable a, Variable b) { Contract.Assert(a.UniqueId != b.UniqueId || a == b); return a.UniqueId < b.UniqueId; diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index f0e2e7ed..b220b373 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -783,7 +783,7 @@ namespace Microsoft.Boogie { public static Graph/*!*/ GraphFromImpl(Implementation impl) { Contract.Requires(impl != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>().TopologicalSort())); + Contract.Ensures(cce.NonNullElements(Contract.Result>().Nodes)); Contract.Ensures(Contract.Result>() != null); Graph g = new Graph(); diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 06d72ee9..e2bbcdf5 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -271,6 +271,7 @@ namespace Microsoft.Boogie { current.Next = other; } // Look for {:name string} in list of attributes. + [Pure] public static string FindStringAttribute(QKeyValue kv, string name) { Contract.Requires(name != null); for (; kv != null; kv = kv.Next) { diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index b89219a9..bdfefb04 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -132,26 +132,23 @@ namespace Microsoft.Boogie { } } - if (false /*CommandLineOptions.Clo.Trace*/) { - - Console.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count); - foreach (Procedure/*!*/ x in modSets.Keys) - { - Contract.Assert(x != null); - Console.Write("{0} : ", x.Name); - bool first = true; - foreach (Variable/*!*/ y in modSets[x]) - { - Contract.Assert(y != null); - if (first) - first = false; - else - Console.Write(", "); - Console.Write("{0}", y.Name); - } - Console.WriteLine(""); - } +#if DEBUG_PRINT + Console.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count); + foreach (Procedure/*!*/ x in modSets.Keys) { + Contract.Assert(x != null); + Console.Write("{0} : ", x.Name); + bool first = true; + foreach (Variable/*!*/ y in modSets[x]) { + Contract.Assert(y != null); + if (first) + first = false; + else + Console.Write(", "); + Console.Write("{0}", y.Name); + } + Console.WriteLine(""); } +#endif } public override Implementation VisitImplementation(Implementation node) { @@ -722,7 +719,7 @@ namespace Microsoft.Boogie { public Implementation/*!*/ impl; [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(graph.TopologicalSort())); + Contract.Invariant(cce.NonNullElements(graph.Nodes)); Contract.Invariant(cce.NonNullDictionaryAndValues(procsCalled)); Contract.Invariant(cce.NonNullElements(nodes)); Contract.Invariant(cce.NonNullDictionaryAndValues(succEdges)); @@ -892,7 +889,7 @@ namespace Microsoft.Boogie { Contract.Invariant(cce.NonNullDictionaryAndValues(name2Proc)); Contract.Invariant(cce.NonNullDictionaryAndValues(callers) && Contract.ForAll(callers.Values, v => cce.NonNullElements(v))); - Contract.Invariant(cce.NonNullElements(callGraph.TopologicalSort())); + Contract.Invariant(cce.NonNullElements(callGraph.Nodes)); Contract.Invariant(procPriority != null); Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveAtEntry)); Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveAtExit) && diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index a11c93ec..650bb146 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -370,9 +370,9 @@ namespace Microsoft.Boogie { } public override YieldCmd VisitYieldCmd(YieldCmd node) { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - return base.VisitYieldCmd((YieldCmd)node.Clone()); + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + return base.VisitYieldCmd((YieldCmd)node.Clone()); } } diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index e883d0bd..b05a2e5f 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -248,8 +248,6 @@ namespace Microsoft.Boogie.Houdini { public class InlineRequiresVisitor : StandardVisitor { public override List VisitCmdSeq(List cmdSeq) { - Contract.Requires(cmdSeq != null); - Contract.Ensures(Contract.Result>() != null); List newCmdSeq = new List(); for (int i = 0, n = cmdSeq.Count; i < n; i++) { Cmd cmd = cmdSeq[i]; @@ -289,8 +287,6 @@ namespace Microsoft.Boogie.Houdini { } public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) { - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); node.Requires = base.VisitRequires(node.Requires); node.Expr = this.VisitExpr(node.Expr); return node; diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index b0be1072..49ae68e3 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2306,7 +2306,7 @@ namespace VC { Contract.Requires(taskID == -1); int inductionK = CommandLineOptions.Clo.KInductionDepth; - Contract.Requires(inductionK >= 0); + Contract.Assume(inductionK >= 0); bool contRuleApplication = true; while (contRuleApplication) { -- cgit v1.2.3