diff options
| author |  wuestholz <unknown> | 2014-07-01 00:55:31 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-07-01 00:55:31 +0200 |
| commit | c5b2aec063fc1f3d5e61ff1b14983c5e4ba7c2ea (patch) | |
| tree | 0610cc62b15151536bba7fdd237a67e4a7b65fca /Source/DafnyDriver | |
| parent | 62e76ea8117eb87571bf49588464540c8fa02357 (diff) | |
Added support for verifying Dafny program snapshots from the command-line.
Diffstat (limited to 'Source/DafnyDriver')
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 20 |
1 files changed, 17 insertions, 3 deletions
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 8f5b5300..01ee269e 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -99,7 +99,7 @@ namespace Microsoft.Dafny }
- static ExitValue ProcessFiles(List<string/*!*/>/*!*/ fileNames)
+ static ExitValue ProcessFiles(List<string/*!*/>/*!*/ fileNames, bool lookForSnapshots = true)
{
Contract.Requires(cce.NonNullElements(fileNames));
@@ -110,7 +110,21 @@ namespace Microsoft.Dafny {
Console.WriteLine();
Console.WriteLine("-------------------- {0} --------------------", f);
- var ev = ProcessFiles(new List<string> { f });
+ var ev = ProcessFiles(new List<string> { f }, lookForSnapshots);
+ if (exitValue != ev && ev != ExitValue.VERIFIED)
+ {
+ exitValue = ev;
+ }
+ }
+ return exitValue;
+ }
+
+ if (0 < CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)
+ {
+ var snapshotsByVersion = ExecutionEngine.LookForSnapshots(fileNames);
+ foreach (var s in snapshotsByVersion)
+ {
+ var ev = ProcessFiles(new List<string>(s), false);
if (exitValue != ev && ev != ExitValue.VERIFIED)
{
exitValue = ev;
@@ -213,7 +227,7 @@ namespace Microsoft.Dafny ExecutionEngine.CollectModSets(program);
ExecutionEngine.CoalesceBlocks(program);
ExecutionEngine.Inline(program);
- return ExecutionEngine.InferAndVerify(program, stats);
+ return ExecutionEngine.InferAndVerify(program, stats, 1 < Dafny.DafnyOptions.Clo.VerifySnapshots ? "main_program_id" : null);
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected outcome
|