diff options
| author |  wuestholz <unknown> | 2014-09-22 17:35:15 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-09-22 17:35:15 +0200 |
| commit | 2aee97da085688aab58c154e367558b1f139d476 (patch) | |
| tree | 1d0f95865555fae5af0f9479367b986a02d94f74 /Source/ExecutionEngine | |
| parent | e4164dd5c959a5252a0954f980bb900581286707 (diff) | |
Fixed an issue in the verification result caching (recycled errors).
Diffstat (limited to 'Source/ExecutionEngine')
| -rw-r--r-- | Source/ExecutionEngine/VerificationResultCache.cs | 27 |
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.
|