summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/AIFramework/CommonFunctionSymbols.cs18
-rw-r--r--Source/AIFramework/Functional.cs2
-rw-r--r--Source/AIFramework/Polyhedra/LinearConstraintSystem.cs2
-rw-r--r--Source/AIFramework/VariableMap/VariableMapLattice.cs9
-rw-r--r--Source/CodeContractsExtender/cce.cs3
-rw-r--r--Source/Core/AbsyExpr.cs9
-rw-r--r--Source/Core/AbsyType.cs9
-rw-r--r--Source/Core/CommandLineOptions.cs3
-rw-r--r--Source/Core/GraphAlgorithms.cs4
-rw-r--r--Source/ParserHelper/ParserHelper.cs7
-rw-r--r--Source/Provers/Simplify/ProverInterface.cs3
-rw-r--r--Source/VCExpr/NameClashResolver.cs1
-rw-r--r--Source/VCExpr/SimplifyLikeLineariser.cs4
-rw-r--r--Source/VCExpr/TypeErasure.cs4
-rw-r--r--Source/VCExpr/VCExprASTVisitors.cs5
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs2
-rw-r--r--Source/VCGeneration/StratifiedVC.cs1
-rw-r--r--Source/VCGeneration/VC.cs8
18 files changed, 26 insertions, 68 deletions
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<FunctionType>() != 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<AIType>() != 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<AIType>() != 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<FunctionSymbol>() != 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<AIType>() != 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<object>() != 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 t) {
- Contract.Assert(t != null);
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result<T>() != 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<Type/*!*/>();
@@ -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<TypeVariableSeq>() != null);
Contract.Ensures(Contract.Result<TypeVariableSeq>().Length == typeParams.Length);
@@ -3586,11 +3584,6 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
public static readonly TypeParamInstantiation EMPTY =
new SimpleTypeParamInstantiation(new List<TypeVariable/*!*/>(),
new Dictionary<TypeVariable/*!*/, Type/*!*/>());
- [ContractInvariantMethod]
- void EMPTYInvariant() {
- Contract.Invariant(EMPTY != null);
- }
-
// return what formal type parameters there are
public List<TypeVariable/*!*/>/*!*/ 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<Node> : IEnumerable<SCC<Node>/*!*/> {
- private readonly IDictionary<Node/*!*/, object/*!*/>/*!*/ graph;
+ private readonly IDictionary<Node/*!*/, object>/*!*/ 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<string>/*?*/ commonPrefix;
+ private readonly List<string> 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<String>() != 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<string>() != 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<string>() != 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<VCTrigger/*!*/>/*!*/ 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<VCExpr>() != 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<VCExprVar/*!*/, object/*!*/>/*!*/ FreeTermVariables(VCExpr node) {
+ public static Dictionary<VCExprVar/*!*/, object>/*!*/ FreeTermVariables(VCExpr node) {
Contract.Requires(node != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<Dictionary<VCExprVar, object>>()));
+ Contract.Ensures(Contract.Result<Dictionary<VCExprVar, object>>() != null);
+ Contract.Ensures(Contract.ForAll(Contract.Result<Dictionary<VCExprVar, object>>(), 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<Counterexample>/*?*/ 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>() != Outcome.Errors || errors != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(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<UnexpectedProverOutputException>(true);
- Contract.Ensures(Contract.Result<VCExpr>() != 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<string, LazyInliningInfo> 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/*<int, Absy!>*/ 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);
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 00:55:42 +0000