Minor refactoring

5 files changed, 21 insertions, 21 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index d961eb3e..5ed619d6 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1865,14 +1865,14 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public byte[] MD5DependenciesChecksum_;

-    public byte[] MD5DependenciesChecksum

+    public byte[] MD5DependencyChecksum_;

+    public byte[] MD5DependencyChecksum

     {

       get

       {

         Contract.Requires(DependenciesCollected);

 

-        if (MD5DependenciesChecksum_ == null && MD5Checksum != null)

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

         {

           var c = MD5Checksum;

           var transFuncDeps = new HashSet<Function>();

@@ -1918,9 +1918,9 @@ namespace Microsoft.Boogie {
               }

             }

           }

-          MD5DependenciesChecksum_ = c;

+          MD5DependencyChecksum_ = c;

         }

-        return MD5DependenciesChecksum_;

+        return MD5DependencyChecksum_;

       }

     }

 

@@ -1932,16 +1932,16 @@ namespace Microsoft.Boogie {
       }

     }

 

-    string dependenciesChecksum;

-    public string DependenciesChecksum

+    string dependencyChecksum;

+    public string DependencyChecksum

     {

       get

       {

-        if (dependenciesChecksum == null && MD5DependenciesChecksum != null)

+        if (dependencyChecksum == null && MD5DependencyChecksum != null)

         {

-          dependenciesChecksum = BitConverter.ToString(MD5DependenciesChecksum);

+          dependencyChecksum = BitConverter.ToString(MD5DependencyChecksum);

         }

-        return dependenciesChecksum;

+        return dependencyChecksum;

       }

     }

 

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index b16fb1ba..26a28e0e 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1999,7 +1999,7 @@ namespace Microsoft.Boogie {
     public string/*!*/ callee { get; set; }

     public Procedure Proc;

     public LocalVariable AssignedAssumptionVariable;

-    public bool EmitDependenciesChecksum;

+    public bool EmitDependencyChecksum;

 

     // Element of the following lists can be null, which means that

     // the call happens with * as these parameters

@@ -2087,12 +2087,12 @@ namespace Microsoft.Boogie {
         stream.Write(" := ");

       }

       stream.Write(TokenTextWriter.SanitizeIdentifier(callee));

-      if (stream.UseForComputingChecksums && EmitDependenciesChecksum)

+      if (stream.UseForComputingChecksums && EmitDependencyChecksum)

       {

-        var c = Proc.DependenciesChecksum;

+        var c = Proc.DependencyChecksum;

         if (c != null)

         {

-          stream.Write(string.Format("[dependencies_checksum:{0}]", c));

+          stream.Write(string.Format("[dependency_checksum:{0}]", c));

         }

       }

       stream.Write("(");

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 33b3a818..95a11a65 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1804,10 +1804,10 @@ namespace Microsoft.Boogie {
       this.name.Emit(stream, 0xF0, false);

       if (stream.UseForComputingChecksums)

       {

-        var c = Func.DependenciesChecksum;

+        var c = Func.DependencyChecksum;

         if (c != null)

         {

-          stream.Write(string.Format("[dependencies_checksum:{0}]", c));

+          stream.Write(string.Format("[dependency_checksum:{0}]", c));

         }

       }

       stream.Write("(");

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 05c4b44b..a9220a4c 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1066,7 +1066,7 @@ namespace Microsoft.Boogie
       {

         #region Verify the implementation

 

-        verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum, impl.Name, impl.tok, programId);

+        verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependencyChecksum, impl.Name, impl.tok, programId);

 

         using (var vcgen = CreateVCGen(program, checkers))

         {

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index b5f6d1cd..d44aff7f 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -197,7 +197,7 @@ namespace Microsoft.Boogie
       // TODO(wuestholz): Maybe we should speed up this lookup.

       var oldProc = programInCachedSnapshot.TopLevelDeclarations.OfType<Procedure>().FirstOrDefault(p => p.Name == node.Proc.Name);

       if (oldProc != null

-          && oldProc.DependenciesChecksum != node.Proc.DependenciesChecksum

+          && oldProc.DependencyChecksum != node.Proc.DependencyChecksum

           && node.AssignedAssumptionVariable == null)

       {

         if (DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program))

@@ -236,7 +236,7 @@ namespace Microsoft.Boogie
         }

         else

         {

-          node.EmitDependenciesChecksum = true;

+          node.EmitDependencyChecksum = true;

         }

       }

 

@@ -308,7 +308,7 @@ namespace Microsoft.Boogie
       // TODO(wuestholz): Maybe we should speed up this lookup.

       var funcs = newProg.TopLevelDeclarations.OfType<Function>();

       return oldProc.DependenciesCollected

-             && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependenciesChecksum == dep.DependenciesChecksum)));

+             && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum)));

     }

 

     public override Procedure VisitProcedure(Procedure node)

@@ -437,7 +437,7 @@ namespace Microsoft.Boogie
       {

         priority = Priority.MEDIUM;

       }

-      else if (impl.DependenciesChecksum == null || result.DependeciesChecksum != impl.DependenciesChecksum)

+      else if (impl.DependencyChecksum == null || result.DependeciesChecksum != impl.DependencyChecksum)

       {

         priority = Priority.LOW;

       }