From 816e4934fa3acfefae2c44ccb2be931c4d65e037 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Thu, 11 Mar 2010 00:27:39 +0000
Subject: Dafny:  Added stratosphere tests for datatypes--that is, it is now
 checked that every datatype has some value.

---
 Source/DafnyDriver/DafnyDriver.ssc | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Source/DafnyDriver')

diff --git a/Source/DafnyDriver/DafnyDriver.ssc b/Source/DafnyDriver/DafnyDriver.ssc
index f0935199..fa86c6e7 100644
--- a/Source/DafnyDriver/DafnyDriver.ssc
+++ b/Source/DafnyDriver/DafnyDriver.ssc
@@ -205,7 +205,8 @@ namespace Microsoft.Boogie
     {
       using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) {
         Dafny.Program dafnyProgram;
-        string err = Dafny.Main.ParseCheck(fileNames, "synthetic program", out dafnyProgram);
+        string programName = fileNames.Count == 1 ? fileNames[0] : "the program";
+        string err = Dafny.Main.ParseCheck(fileNames, programName, out dafnyProgram);
         if (err != null) {
           ErrorWriteLine(err);
         } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {
-- 
cgit v1.2.3