summaryrefslogtreecommitdiff
path: root/Source/ExecutionEngine
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2014-09-22 17:35:15 +0200
committerGravatar wuestholz <unknown>2014-09-22 17:35:15 +0200
commit2aee97da085688aab58c154e367558b1f139d476 (patch)
tree1d0f95865555fae5af0f9479367b986a02d94f74 /Source/ExecutionEngine
parente4164dd5c959a5252a0954f980bb900581286707 (diff)
Fixed an issue in the verification result caching (recycled errors).
Diffstat (limited to 'Source/ExecutionEngine')
-rw-r--r--Source/ExecutionEngine/VerificationResultCache.cs27
1 files changed, 24 insertions, 3 deletions
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 0a2974c8..55c6ba85 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -147,10 +147,13 @@ namespace Microsoft.Boogie
if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)
{
SetErrorChecksumsInCachedSnapshot(impl, vr);
- var p = ExecutionEngine.CachedProgram(vr.ProgramId);
- if (p != null)
+ if (vr.ProgramId != null)
{
- SetAssertionChecksumsInPreviousSnapshot(impl, p);
+ var p = ExecutionEngine.CachedProgram(vr.ProgramId);
+ if (p != null)
+ {
+ SetAssertionChecksumsInPreviousSnapshot(impl, p);
+ }
}
}
}
@@ -161,6 +164,14 @@ namespace Microsoft.Boogie
else if (priority == Priority.SKIP)
{
run.SkippedImplementationCount++;
+ if (vr.ProgramId != null)
+ {
+ var p = ExecutionEngine.CachedProgram(vr.ProgramId);
+ if (p != null)
+ {
+ SetAssertionChecksums(impl, p);
+ }
+ }
}
}
}
@@ -180,6 +191,16 @@ namespace Microsoft.Boogie
}
}
+ private static void SetAssertionChecksums(Implementation implementation, Program program)
+ {
+ // TODO(wuestholz): Maybe we should speed up this lookup.
+ var implPrevSnap = program.Implementations().FirstOrDefault(i => i.Id == implementation.Id);
+ if (implPrevSnap != null)
+ {
+ implementation.AssertionChecksums = implPrevSnap.AssertionChecksums;
+ }
+ }
+
private static void SetAssertionChecksumsInPreviousSnapshot(Implementation implementation, Program program)
{
// TODO(wuestholz): Maybe we should speed up this lookup.