diff options
author | wuestholz <unknown> | 2014-08-03 13:42:36 +0200 |
---|---|---|
committer | wuestholz <unknown> | 2014-08-03 13:42:36 +0200 |
commit | 0d82fe57a792b4b68826a9b0c72cf386052f1ff0 (patch) | |
tree | 061967f1c0f0dc8c233e3b1e3b5b4e60f7de8aeb | |
parent | fcb95cb3964d4b9d5fa112c72f8971df77df7e0b (diff) |
Minor refactoring
-rw-r--r-- | Source/Core/Absy.cs | 20 | ||||
-rw-r--r-- | Source/Core/AbsyCmd.cs | 8 | ||||
-rw-r--r-- | Source/Core/AbsyExpr.cs | 4 | ||||
-rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 2 | ||||
-rw-r--r-- | Source/ExecutionEngine/VerificationResultCache.cs | 8 |
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;
}
|