diff options
| author |  wuestholz <unknown> | 2013-12-18 11:14:19 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-12-18 11:14:19 +0100 |
| commit | 42d8a89ea406dc001dfd83af2e2d66f5ed813cc7 (patch) | |
| tree | 8f070f6c83aaac5c52016756de016f83a98d2772 /Source/DafnyDriver | |
| parent | 7a4728f23ce2101c1cfb7668c350f5c9c8953f5c (diff) | |
Add support for the /verifySeparately flag in Boogie and change most tests to use it.
Diffstat (limited to 'Source/DafnyDriver')
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index a6256580..10c7e90a 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -97,7 +97,22 @@ namespace Microsoft.Dafny static ExitValue ProcessFiles(List<string/*!*/>/*!*/ fileNames)
{
Contract.Requires(cce.NonNullElements(fileNames));
+
ExitValue exitValue = ExitValue.VERIFIED;
+ if (CommandLineOptions.Clo.VerifySeparately && 1 < fileNames.Count)
+ {
+ foreach (var f in fileNames)
+ {
+ Console.WriteLine("\n-------------------- {0} --------------------", f);
+ var ev = ProcessFiles(new List<string> { f });
+ if (exitValue != ev && ev != ExitValue.VERIFIED)
+ {
+ exitValue = ev;
+ }
+ }
+ return exitValue;
+ }
+
using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) {
Dafny.Program dafnyProgram;
string programName = fileNames.Count == 1 ? fileNames[0] : "the program";
|