From f09bf83d24438d712021ada6fab252b0f7f11986 Mon Sep 17 00:00:00 2001 From: tabarbe Date: Fri, 27 Aug 2010 21:52:03 +0000 Subject: Boogie: Commented out all occurences of repeated inherited contracts - makes fewer error messages when compiling with runtime checking on. --- Source/VCGeneration/Check.cs | 333 +++++++++++++++-------------- Source/VCGeneration/ConditionGeneration.cs | 4 +- Source/VCGeneration/DoomErrorHandler.cs | 6 +- Source/VCGeneration/VC.cs | 40 ++-- Source/VCGeneration/VCDoomed.cs | 6 +- 5 files changed, 202 insertions(+), 187 deletions(-) (limited to 'Source/VCGeneration') diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index d5505dd4..d30c93e9 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -14,26 +14,23 @@ using Microsoft.Boogie.AbstractInterpretation; using Microsoft.Boogie.VCExprAST; using Microsoft.Basetypes; -namespace Microsoft.Boogie -{ +namespace Microsoft.Boogie { /// /// Interface to the theorem prover specialized to Boogie. /// /// This class creates the appropriate background axioms. There /// should be one instance per BoogiePL program. /// - public sealed class Checker - { + public sealed class Checker { [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(gen!=null); + void ObjectInvariant() { + Contract.Invariant(gen != null); Contract.Invariant(thmProver != null); Contract.Invariant(ProverDone != null); -} + } private readonly VCExpressionGenerator gen; - + private ProverInterface thmProver; private CommandLineOptions.BvHandling bitvectors; private int timeout; @@ -50,34 +47,37 @@ void ObjectInvariant() public readonly AutoResetEvent ProverDone = new AutoResetEvent(false); - private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl) - { - if (impl == null) return CommandLineOptions.Clo.Bitvectors; + private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl) { + if (impl == null) + return CommandLineOptions.Clo.Bitvectors; bool force_int = false; bool force_native = false; cce.NonNull(impl.Proc).CheckBooleanAttribute("forceBvInt", ref force_int); impl.Proc.CheckBooleanAttribute("forceBvZ3Native", ref force_native); impl.CheckBooleanAttribute("forceBvInt", ref force_int); impl.CheckBooleanAttribute("forceBvZ3Native", ref force_native); - if (force_native) return CommandLineOptions.BvHandling.Z3Native; - if (force_int) return CommandLineOptions.BvHandling.ToInt; + if (force_native) + return CommandLineOptions.BvHandling.Z3Native; + if (force_int) + return CommandLineOptions.BvHandling.ToInt; return CommandLineOptions.Clo.Bitvectors; } - public bool WillingToHandle(Implementation impl, int timeout) - { + public bool WillingToHandle(Implementation impl, int timeout) { return !closed && timeout == this.timeout && bitvectors == BvHandlingForImpl(impl); } - public VCExpressionGenerator VCExprGen - { - get {Contract.Ensures(Contract.Result() != null); - return this.gen; } + public VCExpressionGenerator VCExprGen { + get { + Contract.Ensures(Contract.Result() != null); + return this.gen; + } } - public ProverInterface TheoremProver - { - get {Contract.Ensures(Contract.Result() != null); - return this.thmProver; } + public ProverInterface TheoremProver { + get { + Contract.Ensures(Contract.Result() != null); + return this.thmProver; + } } ///////////////////////////////////////////////////////////////////////////////// @@ -85,10 +85,9 @@ void ObjectInvariant() private struct ContextCacheKey { [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(program!=null); -} + void ObjectInvariant() { + Contract.Invariant(program != null); + } public readonly Program program; public readonly CommandLineOptions.BvHandling bitvectors; @@ -100,7 +99,8 @@ void ObjectInvariant() this.bitvectors = bitvectors; } - [Pure][Reads(ReadsAttribute.Reads.Nothing)] + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] public override bool Equals(object that) { if (that is ContextCacheKey) { ContextCacheKey thatKey = (ContextCacheKey)that; @@ -121,8 +121,7 @@ void ObjectInvariant() /// /// Constructor. Initialize a checker with the program and log file. /// - public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout) - { + public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout) { Contract.Requires(vcgen != null); Contract.Requires(prog != null); this.bitvectors = BvHandlingForImpl(impl); @@ -143,14 +142,14 @@ void ObjectInvariant() } options.BitVectors = this.bitvectors; - ContextCacheKey key = new ContextCacheKey (prog, this.bitvectors); + ContextCacheKey key = new ContextCacheKey(prog, this.bitvectors); ProverContext ctx; ProverInterface prover; if (vcgen.CheckerCommonState == null) { - vcgen.CheckerCommonState = new Dictionary (); + vcgen.CheckerCommonState = new Dictionary(); } - IDictionary/*!>!*/ cachedContexts = (IDictionary) vcgen.CheckerCommonState; + IDictionary/*!>!*/ cachedContexts = (IDictionary)vcgen.CheckerCommonState; if (cachedContexts.TryGetValue(key, out ctx)) { ctx = (ProverContext)cce.NonNull(ctx).Clone(); @@ -203,7 +202,7 @@ void ObjectInvariant() CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx); cachedContexts.Add(key, cce.NonNull((ProverContext)ctx.Clone())); } - + this.thmProver = prover; this.gen = prover.VCExprGen; @@ -214,8 +213,7 @@ void ObjectInvariant() /// /// Clean-up. /// - public void Close() - { + public void Close() { this.closed = true; thmProver.Close(); } @@ -224,35 +222,37 @@ void ObjectInvariant() /// Push a Verification Condition as an Axiom /// (Required for Doomed Program Point detection) /// - public void PushVCExpr(VCExpr vc) - { + public void PushVCExpr(VCExpr vc) { Contract.Requires(vc != null); //thmProver.Context.AddAxiom(vc); thmProver.PushVCExpression(vc); } - public bool IsBusy - { - get { return busy; } + public bool IsBusy { + get { + return busy; + } } - public bool Closed - { - get { return closed; } + public bool Closed { + get { + return closed; + } } - public bool HasOutput - { - get { return hasOutput; } + public bool HasOutput { + get { + return hasOutput; + } } - public TimeSpan ProverRunTime - { - get { return proverRunTime; } + public TimeSpan ProverRunTime { + get { + return proverRunTime; + } } - private void WaitForOutput(object dummy) - { + private void WaitForOutput(object dummy) { try { outcome = thmProver.CheckOutcome(cce.NonNull(handler)); } catch (UnexpectedProverOutputException e) { @@ -277,20 +277,20 @@ void ObjectInvariant() break; } - Contract.Assert( busy); + Contract.Assert(busy); hasOutput = true; proverRunTime = DateTime.Now - proverStart; ProverDone.Set(); } - - public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler){ + + public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) { Contract.Requires(descriptiveName != null); Contract.Requires(vc != null); Contract.Requires(handler != null); - - Contract.Requires( !IsBusy); - Contract.Assert( !busy); + + Contract.Requires(!IsBusy); + Contract.Assert(!busy); busy = true; hasOutput = false; outputExn = null; @@ -303,11 +303,11 @@ void ObjectInvariant() ThreadPool.QueueUserWorkItem(WaitForOutput); } - public ProverInterface.Outcome ReadOutcome(){ - - Contract.Requires( IsBusy); - Contract.Requires( HasOutput); - Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true); + public ProverInterface.Outcome ReadOutcome() { + + Contract.Requires(IsBusy); + Contract.Requires(HasOutput); + Contract.EnsuresOnThrow(true); hasOutput = false; busy = false; @@ -318,7 +318,7 @@ void ObjectInvariant() return outcome; } } - + // ----------------------------------------------------------------------------------------------- // ----------------------------------------------------------------------------------------------- // ----------------------------------------------------------------------------------------------- @@ -331,21 +331,20 @@ void ObjectInvariant() public Dictionary>/*!*/>/*!*/ definedFunctions; [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(cce.NonNullElements(identifierToPartition)); + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(identifierToPartition)); Contract.Invariant(partitionToIdentifiers != null); - Contract.Invariant(Contract.ForAll(partitionToIdentifiers,i=>cce.NonNullElements(i))); + Contract.Invariant(Contract.ForAll(partitionToIdentifiers, i => cce.NonNullElements(i))); Contract.Invariant(partitionToValue != null); Contract.Invariant(valueToPartition != null); Contract.Invariant(cce.NonNullElements(definedFunctions)); -} + } public ErrorModel(Dictionary identifierToPartition, List> partitionToIdentifiers, List partitionToValue, Dictionary valueToPartition, Dictionary>> definedFunctions) { Contract.Requires(cce.NonNullElements(identifierToPartition)); Contract.Requires(partitionToIdentifiers != null); - Contract.Requires(Contract.ForAll(partitionToIdentifiers,i=>cce.NonNullElements(i))); + Contract.Requires(Contract.ForAll(partitionToIdentifiers, i => cce.NonNullElements(i))); Contract.Requires(partitionToValue != null); Contract.Requires(valueToPartition != null); Contract.Requires(cce.NonNullElements(definedFunctions)); @@ -356,39 +355,41 @@ void ObjectInvariant() this.definedFunctions = definedFunctions; } - public virtual void Print(TextWriter writer) {Contract.Requires(writer != null); } - - public int LookupPartitionValue(int partition) - { - BigNum bignum = (BigNum) cce.NonNull(partitionToValue)[partition]; + public virtual void Print(TextWriter writer) { + Contract.Requires(writer != null); + } + + public int LookupPartitionValue(int partition) { + BigNum bignum = (BigNum)cce.NonNull(partitionToValue)[partition]; return bignum.ToInt; } - - public int LookupControlFlowFunctionAt(int cfc, int id) - { + + public int LookupControlFlowFunctionAt(int cfc, int id) { List> tuples = this.definedFunctions["ControlFlow"]; Contract.Assert(tuples != null); - foreach (List tuple in tuples) - { - if (tuple == null) continue; - if (tuple.Count != 3) continue; + foreach (List tuple in tuples) { + if (tuple == null) + continue; + if (tuple.Count != 3) + continue; if (LookupPartitionValue(tuple[0]) == cfc && LookupPartitionValue(tuple[1]) == id) return LookupPartitionValue(tuple[2]); } - Contract.Assert(false);throw new cce.UnreachableException(); + Contract.Assert(false); + throw new cce.UnreachableException(); return 0; } - + private string LookupSkolemConstant(string name) { Contract.Requires(name != null); Contract.Ensures(Contract.Result() != null); - foreach (string functionName in identifierToPartition.Keys) - { + foreach (string functionName in identifierToPartition.Keys) { Contract.Assert(functionName != null); int index = functionName.LastIndexOf("!"); - if (index == -1) continue; + if (index == -1) + continue; string newFunctionName = cce.NonNull(functionName.Remove(index)); if (newFunctionName.Equals(name)) return functionName; @@ -399,67 +400,62 @@ void ObjectInvariant() Contract.Requires(name != null); Contract.Ensures(Contract.Result() != null); - foreach (string functionName in definedFunctions.Keys) - { + foreach (string functionName in definedFunctions.Keys) { Contract.Assert(functionName != null); int index = functionName.LastIndexOf("!"); - if (index == -1) continue; + if (index == -1) + continue; string newFunctionName = cce.NonNull(functionName.Remove(index)); if (newFunctionName.Equals(name)) return functionName; } return ""; } - public int LookupSkolemFunctionAt(string functionName, List values) - - { - Contract.Requires(functionName!= null); + public int LookupSkolemFunctionAt(string functionName, List values) { + Contract.Requires(functionName != null); Contract.Requires(values != null); string actualFunctionName = LookupSkolemFunction(functionName); Contract.Assert(actualFunctionName != null); - if (actualFunctionName.Equals("")) - { + if (actualFunctionName.Equals("")) { // The skolem function is actually a skolem constant actualFunctionName = LookupSkolemConstant(functionName); - Contract.Assert( !actualFunctionName.Equals("")); + Contract.Assert(!actualFunctionName.Equals("")); return identifierToPartition[actualFunctionName]; } List> tuples = this.definedFunctions[actualFunctionName]; - Contract.Assert( tuples.Count > 0); + Contract.Assert(tuples.Count > 0); // the last tuple is a dummy tuple - for (int n = 0; n < tuples.Count - 1; n++) - { + for (int n = 0; n < tuples.Count - 1; n++) { List tuple = cce.NonNull(tuples[n]); - Contract.Assert( tuple.Count - 1 <= values.Count); - for (int i = 0, j = 0; i < values.Count; i++) - { + Contract.Assert(tuple.Count - 1 <= values.Count); + for (int i = 0, j = 0; i < values.Count; i++) { if (values[i] == tuple[j]) { // succeeded in matching tuple[j] j++; - if (j == tuple.Count-1) return tuple[tuple.Count - 1]; + if (j == tuple.Count - 1) + return tuple[tuple.Count - 1]; } } } - Contract.Assert(false);throw new cce.UnreachableException(); + Contract.Assert(false); + throw new cce.UnreachableException(); return 0; } - - public List/*!>!*/ PartitionsToValues(List args) - { + + public List/*!>!*/ PartitionsToValues(List args) { Contract.Requires(args != null); Contract.Ensures(cce.NonNullElements(Contract.Result>())); List vals = new List(); - foreach(int i in args) - { + foreach (int i in args) { object o = cce.NonNull(partitionToValue[i]); if (o is bool) { vals.Add(o); } else if (o is BigNum) { vals.Add(o); } else if (o is List>) { - List> array = (List>) o; + List> array = (List>)o; List> arrayVal = new List>(); foreach (List tuple in array) { Contract.Assert(tuple != null); @@ -472,30 +468,33 @@ void ObjectInvariant() } vals.Add(arrayVal); } else { - Contract.Assert(false);throw new cce.UnreachableException(); + Contract.Assert(false); + throw new cce.UnreachableException(); } } return vals; } } - public abstract class ProverInterface - { - public enum Outcome { Valid, Invalid, TimeOut, OutOfMemory, Undetermined } - public class ErrorHandler - { - public virtual void OnModel(IList/*!>!*/ labels, ErrorModel errModel) - { + public abstract class ProverInterface { + public enum Outcome { + Valid, + Invalid, + TimeOut, + OutOfMemory, + Undetermined + } + public class ErrorHandler { + public virtual void OnModel(IList/*!>!*/ labels, ErrorModel errModel) { Contract.Requires(cce.NonNullElements(labels)); } - public virtual void OnResourceExceeded(string message) - { - Contract.Requires(message!=null); + public virtual void OnResourceExceeded(string message) { + Contract.Requires(message != null); } public virtual void OnProverWarning(string message) - //modifies Console.Out.*, Console.Error.*; + //modifies Console.Out.*, Console.Error.*; { Contract.Requires(message != null); switch (CommandLineOptions.Clo.PrintProverWarnings) { @@ -508,13 +507,13 @@ void ObjectInvariant() Console.Error.WriteLine("Prover warning: " + message); break; default: - Contract.Assume( false);throw new cce.UnreachableException(); // unexpected case + Contract.Assume(false); + throw new cce.UnreachableException(); // unexpected case } } - public virtual Absy Label2Absy(string label) - { + public virtual Absy Label2Absy(string label) { Contract.Requires(label != null); Contract.Ensures(Contract.Result() != null); @@ -529,26 +528,40 @@ void ObjectInvariant() } public virtual void Close() { } - + /// /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta) /// for now it is only implemented by ProcessTheoremProver and still requires some /// testing /// - public virtual void PushVCExpression(VCExpr vc) {Contract.Requires(vc != null);} - public virtual string VCExpressionToString(VCExpr vc) {Contract.Requires(vc != null);Contract.Ensures(Contract.Result() != null); return ""; } - public virtual void Pop() - {Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);} - public virtual int NumAxiomsPushed() - { return 0; } - public virtual int FlushAxiomsToTheoremProver() - { Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);return 0; } - - - public abstract ProverContext Context { get; } -public abstract VCExpressionGenerator VCExprGen { get; } + public virtual void PushVCExpression(VCExpr vc) { + Contract.Requires(vc != null); + } + public virtual string VCExpressionToString(VCExpr vc) { + Contract.Requires(vc != null); + Contract.Ensures(Contract.Result() != null); + return ""; + } + public virtual void Pop() { + Contract.EnsuresOnThrow(true); + } + public virtual int NumAxiomsPushed() { + return 0; + } + public virtual int FlushAxiomsToTheoremProver() { + Contract.EnsuresOnThrow(true); + return 0; + } + + + public abstract ProverContext Context { + get; + } + public abstract VCExpressionGenerator VCExprGen { + get; + } } - public class ProverInterfaceContracts:ProverInterface{ + public class ProverInterfaceContracts : ProverInterface { public override ProverContext Context { get { Contract.Ensures(Contract.Result() != null); @@ -563,32 +576,34 @@ public abstract VCExpressionGenerator VCExprGen { get; } throw new NotImplementedException(); } } - public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler){/*Contract.Requires(descriptiveName != null);*/ Contract.Requires(vc != null);Contract.Requires(handler != null);throw new NotImplementedException();} + public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) {/*Contract.Requires(descriptiveName != null);*/ + //Contract.Requires(vc != null); + //Contract.Requires(handler != null); + throw new NotImplementedException(); + } [NoDefaultContract] - public override Outcome CheckOutcome(ErrorHandler handler){ - //Contract.Requires(handler != null); - Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true); - throw new NotImplementedException();} + public override Outcome CheckOutcome(ErrorHandler handler) { + //Contract.Requires(handler != null); + Contract.EnsuresOnThrow(true); + throw new NotImplementedException(); + } } - - public class ProverException : Exception - { - public ProverException(string s) : base(s) - { + + public class ProverException : Exception { + public ProverException(string s) + : base(s) { } } - public class UnexpectedProverOutputException : ProverException, Microsoft.Contracts.ICheckedException - { - public UnexpectedProverOutputException(string s) : base(s) - { + public class UnexpectedProverOutputException : ProverException, Microsoft.Contracts.ICheckedException { + public UnexpectedProverOutputException(string s) + : base(s) { } } - public class ProverDiedException : UnexpectedProverOutputException - { - public ProverDiedException() : base("Prover died with no further output, perhaps it ran out of memory or was killed.") - { + public class ProverDiedException : UnexpectedProverOutputException { + public ProverDiedException() + : base("Prover died with no further output, perhaps it ran out of memory or was killed.") { } } } diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 209248ed..90ed5d5c 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -722,12 +722,12 @@ namespace VC { public readonly List/*!>!*/ examples = new List(); public override void OnCounterexample(Counterexample ce, string/*?*/ reason) { - Contract.Requires(ce != null); + //Contract.Requires(ce != null); examples.Add(ce); } public override void OnUnreachableCode(Implementation impl) { - Contract.Requires(impl != null); + //Contract.Requires(impl != null); System.Console.WriteLine("found unreachable code:"); EmitImpl(impl, false); // TODO report error about next to last in seq diff --git a/Source/VCGeneration/DoomErrorHandler.cs b/Source/VCGeneration/DoomErrorHandler.cs index 0bcf15f8..12936c1f 100644 --- a/Source/VCGeneration/DoomErrorHandler.cs +++ b/Source/VCGeneration/DoomErrorHandler.cs @@ -41,7 +41,7 @@ void ObjectInvariant() } public override Absy Label2Absy(string label) { - Contract.Requires(label != null); + //Contract.Requires(label != null); Contract.Ensures(Contract.Result() != null); int id = int.Parse(label); @@ -49,7 +49,7 @@ void ObjectInvariant() } public override void OnProverWarning(string msg) { - Contract.Requires(msg != null); + //Contract.Requires(msg != null); this.callback.OnWarning(msg); } @@ -75,7 +75,7 @@ void ObjectInvariant() } public override void OnModel(IList/*!>!*/ labels, ErrorModel errModel) { - Contract.Requires(labels != null); + //Contract.Requires(labels != null); m_CurrentTrace.Clear(); //Console.Write("Used Blocks: "); diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 9ca934b2..a053a153 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -780,7 +780,7 @@ namespace VC { } public override Absy Label2Absy(string label) { - Contract.Requires(label != null); + //Contract.Requires(label != null); Contract.Ensures(Contract.Result() != null); int id = int.Parse(label); @@ -788,7 +788,7 @@ namespace VC { } public override void OnProverWarning(string msg) { - Contract.Requires(msg != null); + //Contract.Requires(msg != null); this.callback.OnWarning(msg); } } @@ -1721,9 +1721,9 @@ namespace VC { } public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback){ - Contract.Requires(impl != null); - Contract.Requires(program != null); - Contract.Requires(callback != null); + //Contract.Requires(impl != null); + //Contract.Requires(program != null); + //Contract.Requires(callback != null); Contract.EnsuresOnThrow(true); if (impl.SkipVerification) { return Outcome.Inconclusive; // not sure about this one @@ -1888,9 +1888,9 @@ namespace VC { } public override Outcome StratifiedVerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback){ - Contract.Requires(impl != null); - Contract.Requires(program != null); - Contract.Requires(callback != null); + //Contract.Requires(impl != null); + //Contract.Requires(program != null); + //Contract.Requires(callback != null); Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true); // This flag control the nature of queries made by StratifiedVerifyImplementation // true: incremental search; false: in-place inlining @@ -2738,8 +2738,8 @@ namespace VC { bool changed, bool arg) { - Contract.Requires(originalNode != null); - Contract.Requires(cce.NonNullElements(newSubExprs)); + //Contract.Requires(originalNode != null); + //Contract.Requires(cce.NonNullElements(newSubExprs)); Contract.Ensures(Contract.Result() != null); VCExpr ret; @@ -2821,7 +2821,7 @@ namespace VC { bool changed, bool arg) { - Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null); + //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null); Contract.Ensures(Contract.Result() != null); VCExpr ret; @@ -2911,7 +2911,7 @@ namespace VC { } public override void OnModel(IList/*!*/ labels, ErrorModel errModel) { - Contract.Requires(cce.NonNullElements(labels)); + //Contract.Requires(cce.NonNullElements(labels)); if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) { errModel.Print(ErrorReporter.ModelWriter); ErrorReporter.ModelWriter.Flush(); @@ -2955,7 +2955,7 @@ namespace VC { } public override Absy Label2Absy(string label) { - Contract.Requires(label != null); + //Contract.Requires(label != null); Contract.Ensures(Contract.Result() != null); int id = int.Parse(label); @@ -2963,12 +2963,12 @@ namespace VC { } public override void OnResourceExceeded(string msg) { - Contract.Requires(msg != null); + //Contract.Requires(msg != null); resourceExceededMessage = msg; } public override void OnProverWarning(string msg) { - Contract.Requires(msg != null); + //Contract.Requires(msg != null); callback.OnWarning(msg); } } @@ -2996,7 +2996,7 @@ namespace VC { } public override void OnModel(IList/*!*/ labels, ErrorModel errModel) { - Contract.Requires(cce.NonNullElements(labels)); + //Contract.Requires(cce.NonNullElements(labels)); // We ignore the error model here for enhanced error message purposes. // It is only printed to the command line. if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) { @@ -3092,7 +3092,7 @@ namespace VC { } public override void OnModel(IList/*!*/ labels, ErrorModel errModel) { - Contract.Requires(cce.NonNullElements(labels)); + //Contract.Requires(cce.NonNullElements(labels)); if (underapproximationMode) { if (errModel == null) return; @@ -3266,7 +3266,7 @@ namespace VC { } public override Absy Label2Absy(string label) { - Contract.Requires(label != null); + //Contract.Requires(label != null); Contract.Ensures(Contract.Result() != null); int id = int.Parse(label); @@ -3285,12 +3285,12 @@ namespace VC { } public override void OnResourceExceeded(string msg) { - Contract.Requires(msg != null); + //Contract.Requires(msg != null); //resourceExceededMessage = msg; } public override void OnProverWarning(string msg) { - Contract.Requires(msg != null); + //Contract.Requires(msg != null); callback.OnWarning(msg); } } diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs index 12543cd5..c1547009 100644 --- a/Source/VCGeneration/VCDoomed.cs +++ b/Source/VCGeneration/VCDoomed.cs @@ -283,9 +283,9 @@ namespace VC { /// /// public override Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback) { - Contract.Requires(impl != null); - Contract.Requires(program != null); - Contract.Requires(callback != null); + //Contract.Requires(impl != null); + //Contract.Requires(program != null); + //Contract.Requires(callback != null); Contract.EnsuresOnThrow(true); UseItAsDebugger = CommandLineOptions.Clo.useDoomDebug; -- cgit v1.2.3