diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 5 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 18 |
2 files changed, 14 insertions, 9 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index d1f09d2a..92be2e0a 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1036,12 +1036,13 @@ namespace Microsoft.Boogie Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(printTimes));
Console.Out.WriteLine("Statistics per request as CSV:");
- Console.Out.WriteLine("Request ID{0}, Error, Inconclusive, Out of Memory, Timeout, Verified, DoNothing, MarkAsPartiallyVerified, MarkAsFullyVerified, RecycleError, AssumeNegationOfAssumptionVariable, Drop", printTimes ? ", Time (ms)" : "");
+ var actions = string.Join(", ", Enum.GetNames(typeof(VC.ConditionGeneration.CachingAction)));
+ Console.Out.WriteLine("Request ID{0}, Error, Inconclusive, Out of Memory, Timeout, Verified, {1}", printTimes ? ", Time (ms)" : "", actions);
foreach (var kv in TimePerRequest.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key)))
{
var s = StatisticsPerRequest[kv.Key];
var cacs = s.CachingActionCounts;
- var c = cacs != null ? string.Format(", {0,3}, {1,3}, {2,3}, {3,3}, {4,3}, {5,3}", cacs[0], cacs[1], cacs[2], cacs[3], cacs[4], cacs[5]) : "";
+ var c = cacs != null ? ", " + cacs.Select(ac => string.Format("{0,3}", ac)).Concat(", ") : "";
var t = printTimes ? string.Format(", {0,8:F0}", kv.Value.TotalMilliseconds) : "";
Console.Out.WriteLine("{0,-19}{1}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}{7}", kv.Key, t, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount, c);
}
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
|