diff options
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 51 | ||||
| -rw-r--r-- | Source/ExecutionEngine/VerificationResultCache.cs | 15 |
2 files changed, 37 insertions, 29 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 2af65733..74d299d1 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -435,28 +435,7 @@ namespace Microsoft.Boogie if (0 < CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)
{
- var snapshotsByVersion = new List<List<string>>();
- for (int version = 0; true; version++)
- {
- var nextSnapshot = new List<string>();
- foreach (var name in fileNames)
- {
- var versionedName = name.Replace(Path.GetExtension(name), ".v" + version + Path.GetExtension(name));
- if (File.Exists(versionedName))
- {
- nextSnapshot.Add(versionedName);
- }
- }
- if (nextSnapshot.Any())
- {
- snapshotsByVersion.Add(nextSnapshot);
- }
- else
- {
- break;
- }
- }
-
+ var snapshotsByVersion = LookForSnapshots(fileNames);
foreach (var s in snapshotsByVersion)
{
ProcessFiles(new List<string>(s), false);
@@ -527,6 +506,34 @@ namespace Microsoft.Boogie }
}
+ public static List<List<string>> LookForSnapshots(List<string> fileNames)
+ {
+ Contract.Requires(fileNames != null);
+
+ var result = new List<List<string>>();
+ for (int version = 0; true; version++)
+ {
+ var nextSnapshot = new List<string>();
+ foreach (var name in fileNames)
+ {
+ var versionedName = name.Replace(Path.GetExtension(name), ".v" + version + Path.GetExtension(name));
+ if (File.Exists(versionedName))
+ {
+ nextSnapshot.Add(versionedName);
+ }
+ }
+ if (nextSnapshot.Any())
+ {
+ result.Add(nextSnapshot);
+ }
+ else
+ {
+ break;
+ }
+ }
+ return result;
+ }
+
public static void CoalesceBlocks(Program program)
{
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index 8eada755..60a6555a 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -16,6 +16,7 @@ namespace Microsoft.Boogie {
public DateTime Start { get; internal set; }
public DateTime End { get; internal set; }
+ public int RewrittenImplementationCount { get; internal set; }
public int ImplementationCount { get; internal set; }
}
@@ -33,24 +34,24 @@ namespace Microsoft.Boogie {
var wr = new StringWriter();
wr.WriteLine("");
- wr.WriteLine("Cached verification result injector statistics:");
+ wr.WriteLine("Cached verification result injector statistics as CSV:");
if (printTime)
{
- wr.WriteLine("Request ID, Time, Implementations (ms)");
+ wr.WriteLine("Request ID, Time (ms), Rewritten Implementations, Implementations");
}
else
{
- wr.WriteLine("Request ID, Implementations (ms)");
+ wr.WriteLine("Request ID, Rewritten Implementations, Implementations");
}
foreach (var kv in runs)
{
if (printTime)
{
- wr.WriteLine("{0}, {1}, {2}", kv.Key, kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds, kv.Value.ImplementationCount);
+ wr.WriteLine("{0}, {1}, {2}, {3}", kv.Key, kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds, kv.Value.RewrittenImplementationCount, kv.Value.ImplementationCount);
}
else
{
- wr.WriteLine("{0}, {1}", kv.Key, kv.Value.ImplementationCount);
+ wr.WriteLine("{0}, {1}, {2}", kv.Key, kv.Value.RewrittenImplementationCount, kv.Value.ImplementationCount);
}
}
return wr.ToString();
@@ -111,7 +112,7 @@ namespace Microsoft.Boogie {
var eai = new CachedVerificationResultInjector(program, implementations);
- var run = new CachedVerificationResultInjectorRun { Start = DateTime.UtcNow };
+ var run = new CachedVerificationResultInjectorRun { Start = DateTime.UtcNow, ImplementationCount = implementations.Count() };
foreach (var impl in implementations)
{
int priority;
@@ -134,7 +135,7 @@ namespace Microsoft.Boogie if (p != null)
{
eai.Inject(impl, p);
- run.ImplementationCount++;
+ run.RewrittenImplementationCount++;
}
}
}
|