diff options
| author |  wuestholz <unknown> | 2014-06-28 17:55:20 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-06-28 17:55:20 +0200 |
| commit | 82375bbf46b54207fc2efcc2ac42bace5fc5e92d (patch) | |
| tree | 128a64c30bcb1cc2dc7f425a4cead07becbd7649 /Source/ExecutionEngine/ExecutionEngine.cs | |
| parent | b3c1b63ae910ec9df00594d7d14e852cf7e709e5 (diff) | |
Changed the verification result cache to use the built-in 'MemoryCache' class.
Diffstat (limited to 'Source/ExecutionEngine/ExecutionEngine.cs')
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index cac56c4b..2b122f8f 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1001,12 +1001,13 @@ namespace Microsoft.Boogie printer.Inform("", output); // newline
printer.Inform(string.Format("Verifying {0} ...", impl.Name), output);
+ int priority = 0;
if (0 < CommandLineOptions.Clo.VerifySnapshots)
{
- verificationResult = Cache.Lookup(impl);
+ verificationResult = Cache.Lookup(impl, out priority);
}
- if (verificationResult != null)
+ if (verificationResult != null && priority == Priority.SKIP)
{
if (CommandLineOptions.Clo.XmlSink != null)
{
@@ -1096,7 +1097,7 @@ namespace Microsoft.Boogie if (0 < CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))
{
- Cache.Insert(impl.Id, verificationResult);
+ Cache.Insert(impl, verificationResult);
}
#endregion
|