diff options
| author |  wuestholz <unknown> | 2014-11-03 10:16:48 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-11-03 10:16:48 +0100 |
| commit | 9a033a6dd23183138116c92a4cae06c4448e4247 (patch) | |
| tree | adf01a74624b6db8ccaabbc674fdba4d2706750b /Source/VCGeneration | |
| parent | 5964ffcfd89533b83b4b381b894194c76b94c84f (diff) | |
Worked on the verification result caching.
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 8f4ac550..9a2a9117 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1475,12 +1475,13 @@ namespace VC { public enum CachingAction : byte
{
- DoNothing,
+ DoNothingToAssert,
MarkAsPartiallyVerified,
MarkAsFullyVerified,
RecycleError,
AssumeNegationOfAssumptionVariable,
- Drop,
+ DropAssume,
+ DropAssert
}
public long[] CachingActionCounts;
@@ -1547,14 +1548,17 @@ namespace VC { var alwaysUseSubsumption = subsumption == CommandLineOptions.SubsumptionOption.Always;
if (currentImplementation != null
&& currentImplementation.HasCachedSnapshot
+ && checksum != null
+ && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)
&& !currentImplementation.AnyErrorsInCachedSnapshot
- && currentImplementation.InjectedAssumptionVariables.Count == 1)
+ && currentImplementation.InjectedAssumptionVariables.Count == 1
+ && relevantAssumpVars.Count == 1)
{
- TraceCachingAction(pc, CachingAction.DoNothing);
+ TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);
}
else if (relevantDoomedAssumpVars.Any())
{
- TraceCachingAction(pc, CachingAction.DoNothing);
+ TraceCachingAction(pc, CachingAction.DoNothingToAssert);
}
else if (currentImplementation != null
&& currentImplementation.HasCachedSnapshot
@@ -1610,7 +1614,7 @@ namespace VC { }
else
{
- TraceCachingAction(pc, CachingAction.DoNothing);
+ TraceCachingAction(pc, CachingAction.DoNothingToAssert);
}
}
else if (pc is AssumeCmd
@@ -1646,7 +1650,7 @@ namespace VC { }
else
{
- TraceCachingAction(pc, CachingAction.Drop);
+ TraceCachingAction(pc, pc is AssumeCmd ? CachingAction.DropAssume : CachingAction.DropAssert);
}
}
#endregion
|