diff options
| -rw-r--r-- | Source/VCGeneration/Check.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/Context.cs | 10 |
3 files changed, 9 insertions, 9 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index a17cea23..d5505dd4 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -563,10 +563,10 @@ 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.Requires(handler != null);
Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);
throw new NotImplementedException();}
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index dea7a445..23f5c804 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -109,8 +109,8 @@ namespace Microsoft.Boogie { public class CounterexampleComparer : IComparer<Counterexample> {
public int Compare(Counterexample c1, Counterexample c2) {
- Contract.Requires(c1 != null);
- Contract.Requires(c2 != null);
+ //Contract.Requires(c1 != null);
+ //Contract.Requires(c2 != null);
if (c1.GetLocation() == c2.GetLocation())
return 0;
if (c1.GetLocation() > c2.GetLocation())
diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs index 928dd4a6..66f1e9a1 100644 --- a/Source/VCGeneration/Context.cs +++ b/Source/VCGeneration/Context.cs @@ -164,7 +164,7 @@ void ObjectInvariant() protected override void ProcessDeclaration(Declaration decl)
{
- Contract.Requires(decl != null);
+ //Contract.Requires(decl != null);
for (QKeyValue a = decl.Attributes; a != null; a = a.Next) {
if (a.Key == "prover" && a.Params.Count == 1) {
string cmd = a.Params[0] as string;
@@ -180,11 +180,11 @@ void ObjectInvariant() }
}
- public override void DeclareFunction(Function f, string attributes) {Contract.Requires(f != null);
+ public override void DeclareFunction(Function f, string attributes) {//Contract.Requires(f != null);
base.ProcessDeclaration(f);
}
- public override void DeclareConstant(Constant c, bool uniq, string attributes) {Contract.Requires(c != null);
+ public override void DeclareConstant(Constant c, bool uniq, string attributes) {//Contract.Requires(c != null);
base.DeclareConstant(c, uniq, attributes);
orderingAxiomBuilder.AddConstant(c);
@@ -195,7 +195,7 @@ void ObjectInvariant() }
}
- public override void AddAxiom(Axiom ax, string attributes) {Contract.Requires(ax != null);
+ public override void AddAxiom(Axiom ax, string attributes) {//Contract.Requires(ax != null);
base.AddAxiom(ax, attributes);
string ignore = ax.FindStringAttribute("ignore");
@@ -207,7 +207,7 @@ void ObjectInvariant() }
public override void AddAxiom(VCExpr vc)
- {Contract.Requires(vc != null);
+ {//Contract.Requires(vc != null);
axiomConjuncts.Add(vc);
}
|