diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 31 | ||||
| -rw-r--r-- | Test/snapshots/Answer | 28 |
2 files changed, 35 insertions, 24 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index a39e8696..be1266b2 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -161,16 +161,27 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)
{
- var snapshots =
- from n in fileNames
- from f in Directory.GetFiles(Path.GetDirectoryName(Path.GetFullPath(n)), Path.GetFileNameWithoutExtension(n) + ".*" + Path.GetExtension(n))
- select f;
-
- var snapshotsByVersion =
- from n in snapshots
- group n by Path.GetFileNameWithoutExtension(n).Substring(Path.GetFileNameWithoutExtension(n).LastIndexOf(".")) into g
- orderby g.Key
- select g;
+ 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;
+ }
+ }
foreach (var s in snapshotsByVersion)
{
diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer index aac9cd03..434cdfda 100644 --- a/Test/snapshots/Answer +++ b/Test/snapshots/Answer @@ -1,27 +1,27 @@ -c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
Execution trace:
- c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): anon0
-c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(8,5): Error BP5001: This assertion might not hold.
+ Snapshots0.v0.bpl(41,5): anon0
+Snapshots0.v0.bpl(8,5): Error BP5001: This assertion might not hold.
Execution trace:
- c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(8,5): anon0
-c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(19,5): Error BP5001: This assertion might not hold.
+ Snapshots0.v0.bpl(8,5): anon0
+Snapshots0.v0.bpl(19,5): Error BP5001: This assertion might not hold.
Execution trace:
- c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(19,5): anon0
-c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(30,5): Error BP5001: This assertion might not hold.
+ Snapshots0.v0.bpl(19,5): anon0
+Snapshots0.v0.bpl(30,5): Error BP5001: This assertion might not hold.
Execution trace:
- c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(30,5): anon0
+ Snapshots0.v0.bpl(30,5): anon0
Boogie program verifier finished with 0 verified, 4 errors
-c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
Execution trace:
- c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): anon0
-c:\dafny\boogie\Test\snapshots\Snapshots0.v1.bpl(30,5): Error BP5001: This assertion might not hold.
+ Snapshots0.v0.bpl(41,5): anon0
+Snapshots0.v1.bpl(30,5): Error BP5001: This assertion might not hold.
Execution trace:
- c:\dafny\boogie\Test\snapshots\Snapshots0.v1.bpl(30,5): anon0
+ Snapshots0.v1.bpl(30,5): anon0
Boogie program verifier finished with 2 verified, 2 errors
-c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
Execution trace:
- c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): anon0
+ Snapshots0.v0.bpl(41,5): anon0
Boogie program verifier finished with 2 verified, 1 error
|