diff options
| author |  rustanleino <unknown> | 2010-03-11 00:27:39 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-03-11 00:27:39 +0000 |
| commit | 816e4934fa3acfefae2c44ccb2be931c4d65e037 (patch) | |
| tree | 4378bbc4f2b3c1cddf33dfdf0c2e9c285791edc6 /Source/DafnyDriver | |
| parent | 6b17a67248e139e140d84bf0eb3156d6f50bf64b (diff) | |
Dafny: Added stratosphere tests for datatypes--that is, it is now checked that every datatype has some value.
Diffstat (limited to 'Source/DafnyDriver')
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.ssc | 3 |
1 files changed, 2 insertions, 1 deletions
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) {
|