From 241de8264a32285d371a53d8d91a219625d76922 Mon Sep 17 00:00:00 2001 From: mikebarnett Date: Mon, 7 Mar 2011 05:15:14 +0000 Subject: Fix contracts so runtime checking can be turned on. --- Source/AIFramework/CommonFunctionSymbols.cs | 18 ++---------------- Source/AIFramework/Functional.cs | 2 +- Source/AIFramework/Polyhedra/LinearConstraintSystem.cs | 2 +- Source/AIFramework/VariableMap/VariableMapLattice.cs | 9 ++------- Source/CodeContractsExtender/cce.cs | 3 ++- Source/Core/AbsyExpr.cs | 9 ++------- Source/Core/AbsyType.cs | 9 +-------- Source/Core/CommandLineOptions.cs | 3 +-- Source/Core/GraphAlgorithms.cs | 4 ++-- Source/ParserHelper/ParserHelper.cs | 7 +------ Source/Provers/Simplify/ProverInterface.cs | 3 +-- Source/VCExpr/NameClashResolver.cs | 1 - Source/VCExpr/SimplifyLikeLineariser.cs | 4 ++-- Source/VCExpr/TypeErasure.cs | 4 ++-- Source/VCExpr/VCExprASTVisitors.cs | 5 +++-- Source/VCGeneration/ConditionGeneration.cs | 2 +- Source/VCGeneration/StratifiedVC.cs | 1 - Source/VCGeneration/VC.cs | 8 ++------ 18 files changed, 26 insertions(+), 68 deletions(-) (limited to 'Source') diff --git a/Source/AIFramework/CommonFunctionSymbols.cs b/Source/AIFramework/CommonFunctionSymbols.cs index 7dbfdd03..d8e4497f 100644 --- a/Source/AIFramework/CommonFunctionSymbols.cs +++ b/Source/AIFramework/CommonFunctionSymbols.cs @@ -220,15 +220,6 @@ Contract.Ensures(Contract.Result() != null); } [Once] private static AIType/*!*/ binreltype; - [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(binreltype != null); - Contract.Invariant(_eq != null); - Contract.Invariant(_neq != null); - Contract.Invariant(_subtype != null); - Contract.Invariant(_typeof != null); -} private static AIType/*!*/ BinrelType { get {Contract.Ensures(Contract.Result() != null); @@ -462,7 +453,7 @@ Contract.Requires(f != null); private static readonly AIType/*!*/ heaptype = new Heap(); public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result() != null); return heaptype; } } - // the types in the following, select1, select2, are hard-coded; + // the types in the following, select1, select2, are hard-coded; // these types may not always be appropriate private static readonly FunctionSymbol/*!*/ _select1 = new FunctionSymbol("sel1", // Heap x FieldName -> Prop @@ -476,7 +467,7 @@ Contract.Requires(f != null); ); public static FunctionSymbol/*!*/ Select2 { get {Contract.Ensures(Contract.Result() != null); return _select2; } } - // the types in the following, store1, store2, are hard-coded; + // the types in the following, store1, store2, are hard-coded; // these types may not always be appropriate private static readonly FunctionSymbol/*!*/ _update1 = new FunctionSymbol("upd1", // Heap x FieldName x Value -> Heap @@ -626,11 +617,6 @@ Contract.Requires(f != null); public sealed class Prop : AIType { private static readonly AIType/*!*/ proptype = new Prop(); - [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(proptype != null); -} public static AIType/*!*/ Type { get {Contract.Ensures(Contract.Result() != null); return proptype; } } diff --git a/Source/AIFramework/Functional.cs b/Source/AIFramework/Functional.cs index 531ce94f..3b8237bf 100644 --- a/Source/AIFramework/Functional.cs +++ b/Source/AIFramework/Functional.cs @@ -111,7 +111,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections { object IFunctionalMap.this[object key] { get { - Contract.Ensures(Contract.Result() != null); + Contract.Requires(key != null); throw new System.NotImplementedException(); } } diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs index b6ce193a..299d49cf 100644 --- a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs +++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs @@ -1273,7 +1273,7 @@ Contract.Requires(oldName != null); static void SimplifyFrameElements(ArrayList/*!*/ /*FrameElement*/ ff, bool vertices, ArrayList/*!*/ /*LinearConstraint*/ constraints, out SimplificationStatus[]/*!*/ status) { Contract.Requires(ff != null); Contract.Requires(constraints != null); - Contract.Requires(Contract.ValueAtReturn(out status) != null); + Contract.Ensures(Contract.ValueAtReturn(out status) != null); status = new SimplificationStatus[ff.Count]; bool[,] sat = new bool[ff.Count, constraints.Count]; for (int i = 0; i < ff.Count; i++) { diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.cs b/Source/AIFramework/VariableMap/VariableMapLattice.cs index b3c702d7..b60d318b 100644 --- a/Source/AIFramework/VariableMap/VariableMapLattice.cs +++ b/Source/AIFramework/VariableMap/VariableMapLattice.cs @@ -64,13 +64,8 @@ namespace Microsoft.AbstractInterpretationFramework { return s + "]"; } - public static Elt/*!*/ Top = new Elt(true); - public static Elt/*!*/ Bottom = new Elt(false); - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Top != null); - Contract.Invariant(Bottom != null); - } + public static readonly Elt/*!*/ Top = new Elt(true); + public static readonly Elt/*!*/ Bottom = new Elt(false); public Elt(IFunctionalMap constraints) { diff --git a/Source/CodeContractsExtender/cce.cs b/Source/CodeContractsExtender/cce.cs index ef594484..64b6527a 100644 --- a/Source/CodeContractsExtender/cce.cs +++ b/Source/CodeContractsExtender/cce.cs @@ -16,7 +16,8 @@ public static class cce { //} [Pure] public static T NonNull(T t) { - Contract.Assert(t != null); + Contract.Requires(t != null); + Contract.Ensures(Contract.Result() != null); return t; } [Pure] diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 7d01bc8f..630f6f14 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1063,12 +1063,7 @@ namespace Microsoft.Boogie { } } private sealed class OldFunctionSymbol : AI.IFunctionSymbol { - private static AI.AIType/*!*/ aitype = new AI.FunctionType(AI.Value.Type, AI.Value.Type); - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(aitype != null); - Contract.Invariant(Sym != null); - } + private static readonly AI.AIType/*!*/ aitype = new AI.FunctionType(AI.Value.Type, AI.Value.Type); public AI.AIType/*!*/ AIType { get { @@ -1078,7 +1073,7 @@ namespace Microsoft.Boogie { } private OldFunctionSymbol() { } - internal static OldFunctionSymbol/*!*/ Sym = new OldFunctionSymbol(); + internal static readonly OldFunctionSymbol/*!*/ Sym = new OldFunctionSymbol(); [Pure] public override string ToString() { diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 288f5769..96bf358e 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -515,7 +515,6 @@ namespace Microsoft.Boogie { Contract.Requires(formalIns != null); Contract.Requires(formalOuts != null); Contract.Requires(actualIns != null); - Contract.Requires(actualOuts != null); Contract.Requires(typeCheckingSubject != null); Contract.Requires(opName != null);Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out actualTypeParams))); actualTypeParams = new List(); @@ -679,7 +678,6 @@ namespace Microsoft.Boogie { public static TypeVariableSeq/*!*/ SortTypeParams(TypeVariableSeq/*!*/ typeParams, TypeSeq/*!*/ argumentTypes, Type resultType) { Contract.Requires(typeParams != null); Contract.Requires(argumentTypes != null); - Contract.Requires(resultType != null); Contract.Ensures(Contract.Result() != null); Contract.Ensures(Contract.Result().Length == typeParams.Length); @@ -3586,11 +3584,6 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); public static readonly TypeParamInstantiation EMPTY = new SimpleTypeParamInstantiation(new List(), new Dictionary()); - [ContractInvariantMethod] - void EMPTYInvariant() { - Contract.Invariant(EMPTY != null); - } - // return what formal type parameters there are public List/*!*/ FormalTypeParams { @@ -3626,7 +3619,7 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); void ObjectInvariant() { Contract.Invariant(Proxy != null); Contract.Invariant(ArgumentsResult != null); - Contract.Invariant(cce.NonNullElements(Instantiations)); + Contract.Invariant(Instantiations == null || cce.NonNullElements(Instantiations)); } diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 0bc1bce2..2fb29d7a 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -52,7 +52,6 @@ namespace Microsoft.Boogie { void ObjectInvariant() { Contract.Invariant(_toolname != null); Contract.Invariant(_version != null); - Contract.Invariant(Clo != null); Contract.Invariant(Environment != null); Contract.Invariant(FileName != null); Contract.Invariant(cce.NonNullElements(Files)); @@ -73,7 +72,7 @@ namespace Microsoft.Boogie { } } - public static CommandLineOptions/*!*/ Clo = new CommandLineOptions(); // singleton to access all global data + public static readonly CommandLineOptions/*!*/ Clo = new CommandLineOptions(); // singleton to access all global data public string/*!*/ Environment = ""; public string/*!*/ FileName = "unknown"; diff --git a/Source/Core/GraphAlgorithms.cs b/Source/Core/GraphAlgorithms.cs index e901005e..0815e54a 100644 --- a/Source/Core/GraphAlgorithms.cs +++ b/Source/Core/GraphAlgorithms.cs @@ -72,10 +72,10 @@ namespace Microsoft.Boogie { } public sealed class StronglyConnectedComponents : IEnumerable/*!*/> { - private readonly IDictionary/*!*/ graph; + private readonly IDictionary/*!*/ graph; [ContractInvariantMethod] void graphInvariantMethod() { - Contract.Invariant(cce.NonNullElements(graph)); + Contract.Invariant(Contract.ForAll(graph, entry => entry.Key != null)); Contract.Invariant(preds != null); Contract.Invariant(succs != null); } diff --git a/Source/ParserHelper/ParserHelper.cs b/Source/ParserHelper/ParserHelper.cs index 465b9245..a24343c9 100644 --- a/Source/ParserHelper/ParserHelper.cs +++ b/Source/ParserHelper/ParserHelper.cs @@ -47,12 +47,7 @@ namespace Microsoft.Boogie { public string/*!*/ _val; // token value public Token next; // ML 2005-03-11 Tokens are kept in linked list - public static IToken/*!*/ NoToken = new Token(); - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(NoToken != null); - } - + public static readonly IToken/*!*/ NoToken = new Token(); public Token() { this._val = "anything so that it is nonnull"; diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs index 50eefc49..7f7c4686 100644 --- a/Source/Provers/Simplify/ProverInterface.cs +++ b/Source/Provers/Simplify/ProverInterface.cs @@ -66,7 +66,7 @@ namespace Microsoft.Boogie.Simplify { [StrictReadonly] protected readonly ProverOptions options; [StrictReadonly] - private readonly List/*?*/ commonPrefix; + private readonly List commonPrefix; [ContractInvariantMethod] void ObjectInvariant() { @@ -75,7 +75,6 @@ namespace Microsoft.Boogie.Simplify { Contract.Invariant(openActivityString != null); Contract.Invariant(closeActivityString != null); Contract.Invariant(options != null); - Contract.Invariant(cce.NonNullElements(commonPrefix)); } diff --git a/Source/VCExpr/NameClashResolver.cs b/Source/VCExpr/NameClashResolver.cs index 4c6fcbb5..7c06af18 100644 --- a/Source/VCExpr/NameClashResolver.cs +++ b/Source/VCExpr/NameClashResolver.cs @@ -146,7 +146,6 @@ namespace Microsoft.Boogie.VCExprAST { public string this[Object/*!*/ thingie] { get { Contract.Requires(thingie != null); - Contract.Ensures(Contract.Result() != null); string res; for (int i = LocalNames.Count - 1; i >= 0; --i) { diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs index 45eeda43..c907bd9f 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.cs +++ b/Source/VCExpr/SimplifyLikeLineariser.cs @@ -335,14 +335,14 @@ namespace Microsoft.Boogie.VCExprAST { public static string StoreOpName(VCExprNAry node) { Contract.Requires(node != null); - Contract.Requires((node.Op is VCExprStoreOp)); + Contract.Requires((node.Op is VCExprSelectOp) || (node.Op is VCExprStoreOp)); Contract.Ensures(Contract.Result() != null); return "Store_" + TypeToString(node[0].Type); } public static string SelectOpName(VCExprNAry node) { Contract.Requires(node != null); - Contract.Requires((node.Op is VCExprSelectOp)); + Contract.Requires((node.Op is VCExprSelectOp) || (node.Op is VCExprStoreOp)); Contract.Ensures(Contract.Result() != null); return "Select_" + TypeToString(node[0].Type); } diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index 20c946e5..5f3dbc36 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -633,7 +633,7 @@ namespace Microsoft.Boogie.TypeErasure { protected VCExpr GenReverseCastEq(Function castToU, Function castFromU, out VCExprVar var, out List/*!*/ triggers) { Contract.Requires((castFromU != null)); Contract.Requires((castToU != null)); - Contract.Requires((cce.NonNullElements(Contract.ValueAtReturn(out triggers)))); + Contract.Ensures((cce.NonNullElements(Contract.ValueAtReturn(out triggers)))); Contract.Ensures(Contract.ValueAtReturn(out var) != null); Contract.Ensures(Contract.Result() != null); var = Gen.Variable("x", U); @@ -1588,7 +1588,7 @@ namespace Microsoft.Boogie.TypeErasure { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(varsInCasts)); - Contract.Invariant(cce.NonNullElements(varsOutsideCasts)); + Contract.Invariant(varsOutsideCasts != null && Contract.ForAll(varsOutsideCasts, voc => voc.Key != null)); Contract.Invariant(AxBuilder != null); } diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index 3e65ec23..c43ee478 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -634,9 +634,10 @@ namespace Microsoft.Boogie.VCExprAST { return true; } - public static Dictionary/*!*/ FreeTermVariables(VCExpr node) { + public static Dictionary/*!*/ FreeTermVariables(VCExpr node) { Contract.Requires(node != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Contract.Ensures(Contract.Result>() != null); + Contract.Ensures(Contract.ForAll(Contract.Result>(), ftv => ftv.Key != null)); FreeVariableCollector collector = new FreeVariableCollector(); collector.Traverse(node, true); return collector.FreeTermVars; diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 5323bb03..20b17e6b 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -507,8 +507,8 @@ namespace VC { public Outcome VerifyImplementation(Implementation impl, Program program, out List/*?*/ errors) { Contract.Requires(impl != null); Contract.Requires(program != null); - Contract.Requires(Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null)); + Contract.Ensures(Contract.ValueAtReturn(out errors) == null || Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null)); Contract.Ensures(Contract.Result() != Outcome.Errors || errors != null); Contract.EnsuresOnThrow(true); Helpers.ExtraTraceInformation("Starting implementation verification"); diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index c57863a3..c418f828 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1496,7 +1496,6 @@ namespace VC Contract.Requires(vState.calls != null); Contract.Requires(vState.checker != null); Contract.EnsuresOnThrow(true); - Contract.Ensures(Contract.Result() != null); var checker = vState.checker.underlyingChecker; var calls = vState.calls; diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 87f78a96..0215784b 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -73,7 +73,7 @@ namespace VC { Contract.Invariant(controlFlowVariable != null); Contract.Invariant(assertExpr != null); Contract.Invariant(cce.NonNullElements(interfaceVars)); - Contract.Invariant(cce.NonNullElements(incarnationOriginMap)); + Contract.Invariant(incarnationOriginMap == null || cce.NonNullElements(incarnationOriginMap)); } public Implementation impl; @@ -145,7 +145,7 @@ namespace VC { } [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(implName2LazyInliningInfo)); + Contract.Invariant(implName2LazyInliningInfo == null || cce.NonNullElements(implName2LazyInliningInfo)); } private Dictionary implName2LazyInliningInfo; @@ -2678,7 +2678,6 @@ namespace VC { Contract.Requires(b != null); Contract.Requires(traceNodes != null); Contract.Requires(trace != null); - Contract.Requires(errModel != null); Contract.Requires(cce.NonNullElements(incarnationOriginMap)); Contract.Requires(cce.NonNullElements(implName2LazyInliningInfo)); Contract.Requires(context != null); @@ -3525,7 +3524,6 @@ namespace VC { Hashtable/**/ label2absy, ProverContext proverCtxt) { Contract.Requires(startBlock != null); - Contract.Requires(controlFlowVariable != null); Contract.Requires(label2absy != null); Contract.Requires(proverCtxt != null); @@ -3545,7 +3543,6 @@ namespace VC { ProverContext proverCtxt) { Contract.Requires(block != null); - Contract.Requires(controlFlowVariable != null); Contract.Requires(label2absy != null); Contract.Requires(blockVariables!= null); Contract.Requires(cce.NonNullElements(bindings)); @@ -3833,7 +3830,6 @@ namespace VC { Microsoft.Boogie.VCExpressionGenerator gen) { Contract.Requires(b != null); Contract.Requires(BlkCorrect != null); - Contract.Requires(BlkReached != null); Contract.Requires(totalOrder != null); Contract.Requires(g != null); Contract.Requires(context != null); -- cgit v1.2.3