fixed various CodeContracts issues.

5 files changed, 6 insertions, 8 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 86d49859..73e57dc8 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1990,7 +1990,7 @@ namespace Microsoft.Boogie {
     {

       get

       {

-        Contract.Requires(DependenciesCollected);

+        Contract.Requires(CommandLineOptions.Clo.VerifySnapshots == 0 || DependenciesCollected);

 

         if (MD5DependencyChecksum_ == null && MD5Checksum != null)

         {

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 26a28e0e..c7edbc68 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2532,8 +2532,8 @@ namespace Microsoft.Boogie {
 

     NameEqualityComparer comparer = new NameEqualityComparer();

 

-    Substitution calleeSubstitution;

-    Substitution calleeSubstitutionOld;

+    public Substitution calleeSubstitution;

+    public Substitution calleeSubstitutionOld;

 

     public IEnumerable<IdentifierExpr> UnmodifiedBefore(Procedure oldProcedure)

     {

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index f648cec1..4c590ddb 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -212,7 +212,7 @@ namespace Microsoft.Boogie {
 

     public static Expr Neg(Expr e1) {

       Contract.Requires(e1 != null);

-      Contract.Ensures(Contract.Result<NAryExpr>() != null);

+      Contract.Ensures(Contract.Result<Expr>() != null);

       return Unary(Token.NoToken, UnaryOperator.Opcode.Neg, e1);

     }

 

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index d61c9941..98bb95d2 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -364,8 +364,8 @@ namespace Microsoft.Boogie {
       Contract.Invariant(0 <= PrintUnstructured && PrintUnstructured < 3);  // 0 = print only structured,  1 = both structured and unstructured,  2 = only unstructured

     }

 

-    public int VerifySnapshots;

-    public bool VerifySeparately;

+    public int VerifySnapshots = 0;

+    public bool VerifySeparately = false;

     public string PrintFile = null;

     public int PrintUnstructured = 0;

     public bool UseBaseNameForFileName = false;

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 81231fd0..d9f53a56 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -804,8 +804,6 @@ namespace VC {
       Contract.Requires(gotoCmdOrigins != null);

       Contract.Requires(impl.Proc != null);

       Contract.Requires(unifiedExitBlock.TransferCmd is ReturnCmd);

-      Contract.Ensures(Contract.Result<Block>() != null);

-      Contract.Ensures(Contract.Result<Block>().TransferCmd is ReturnCmd);

 

       TokenTextWriter debugWriter = null;

       if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {