diff options
| author |  wuestholz <unknown> | 2014-10-14 23:25:26 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-10-14 23:25:26 +0200 |
| commit | 653a174146e9f327568eba090093765c54b00cca (patch) | |
| tree | 6ff27618c4d9808bd666dab59c7a278d5bda1bf7 /Source/VCGeneration | |
| parent | 6b5897a9289102e16a3e24069d1c76278a2e3986 (diff) | |
Made it produce more trace output for the verification result caching.
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 628ceb0f..52db07d9 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1330,7 +1330,20 @@ namespace VC { currentImplementation = impl;
currentTemporaryVariableForAssertions = null;
+
+ var start = DateTime.UtcNow;
+
Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);
+
+ var end = DateTime.UtcNow;
+ if (CommandLineOptions.Clo.TraceCaching)
+ {
+ Console.Out.WriteLine("");
+ Console.Out.WriteLine("<trace caching>");
+ Console.Out.WriteLine("Turned implementation into passive commands within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);
+ Console.Out.WriteLine("</trace caching>");
+ }
+
currentTemporaryVariableForAssertions = null;
currentImplementation = null;
|