diff options
| author |  wuestholz <unknown> | 2014-10-14 23:08:03 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-10-14 23:08:03 +0200 |
| commit | 6b5897a9289102e16a3e24069d1c76278a2e3986 (patch) | |
| tree | 50c3a770369bfa2b9dd7ee40e2e86446339d33d8 /Source/ExecutionEngine | |
| parent | 40c7b73bda334bdfe89e50a0f72d2e3a49e009b4 (diff) | |
Made it produce more trace output for the verification result caching.
Diffstat (limited to 'Source/ExecutionEngine')
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 2 | ||||
| -rw-r--r-- | Source/ExecutionEngine/VerificationResultCache.cs | 22 |
2 files changed, 23 insertions, 1 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 10c5e01a..e00b9b7a 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1017,7 +1017,7 @@ namespace Microsoft.Boogie programCache.Set(programId, program, policy);
}
- if (1 <= CommandLineOptions.Clo.VerifySnapshots && CommandLineOptions.Clo.TraceCaching)
+ if (0 <= CommandLineOptions.Clo.VerifySnapshots && CommandLineOptions.Clo.TraceCaching)
{
Console.Out.WriteLine("");
Console.Out.WriteLine("<trace caching>");
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index af3821c2..1de1a0ce 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -272,6 +272,8 @@ namespace Microsoft.Boogie public static void Collect(IEnumerable<Axiom> axioms)
{
+ var start = DateTime.UtcNow;
+
var v = new OtherDefinitionAxiomsCollector();
foreach (var a in axioms)
{
@@ -279,6 +281,15 @@ namespace Microsoft.Boogie v.VisitExpr(a.Expr);
v.currentAxiom = null;
}
+
+ var end = DateTime.UtcNow;
+ if (CommandLineOptions.Clo.TraceCaching)
+ {
+ Console.Out.WriteLine("");
+ Console.Out.WriteLine("<trace caching>");
+ Console.Out.WriteLine("Collected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);
+ Console.Out.WriteLine("</trace caching>");
+ }
}
public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node)
@@ -317,8 +328,19 @@ namespace Microsoft.Boogie public static void Collect(Program program)
{
+ var start = DateTime.UtcNow;
+
var dc = new DependencyCollector();
dc.VisitProgram(program);
+
+ var end = DateTime.UtcNow;
+ if (CommandLineOptions.Clo.TraceCaching)
+ {
+ Console.Out.WriteLine("");
+ Console.Out.WriteLine("<trace caching>");
+ Console.Out.WriteLine("Collected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);
+ Console.Out.WriteLine("</trace caching>");
+ }
}
public static bool AllFunctionDependenciesAreDefinedAndUnchanged(Procedure oldProc, Program newProg)
|