1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.IO;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using Bpl = Microsoft.Boogie;
namespace Microsoft.Dafny {
public class Main {
private static void MaybePrintProgram(Program program, string filename)
{
if (filename != null) {
TextWriter tw;
if (filename == "-") {
tw = System.Console.Out;
} else {
tw = new System.IO.StreamWriter(filename);
}
Printer pr = new Printer(tw, DafnyOptions.O.PrintMode);
pr.PrintProgram(program);
}
}
/// <summary>
/// Returns null on success, or an error string otherwise.
/// </summary>
public static string ParseCheck(List<string/*!*/>/*!*/ fileNames, string/*!*/ programName, out Program program)
//modifies Bpl.CommandLineOptions.Clo.XmlSink.*;
{
Contract.Requires(programName != null);
Contract.Requires(fileNames != null);
program = null;
ModuleDecl module = new LiteralModuleDecl(new DefaultModuleDecl(), null);
BuiltIns builtIns = new BuiltIns();
foreach (string dafnyFileName in fileNames){
Contract.Assert(dafnyFileName != null);
if (Bpl.CommandLineOptions.Clo.XmlSink != null && Bpl.CommandLineOptions.Clo.XmlSink.IsOpen) {
Bpl.CommandLineOptions.Clo.XmlSink.WriteFileFragment(dafnyFileName);
}
if (Bpl.CommandLineOptions.Clo.Trace)
{
Console.WriteLine("Parsing " + dafnyFileName);
}
string err = ParseFile(dafnyFileName, Bpl.Token.NoToken, module, builtIns, new Errors());
if (err != null) {
return err;
}
}
if (!DafnyOptions.O.DisallowIncludes) {
string errString = ParseIncludes(module, builtIns, fileNames, new Errors());
if (errString != null) {
return errString;
}
}
program = new Program(programName, module, builtIns);
MaybePrintProgram(program, DafnyOptions.O.DafnyPrintFile);
if (Bpl.CommandLineOptions.Clo.NoResolve || Bpl.CommandLineOptions.Clo.NoTypecheck) { return null; }
Dafny.Resolver r = new Dafny.Resolver(program);
r.ResolveProgram(program);
MaybePrintProgram(program, DafnyOptions.O.DafnyPrintResolvedFile);
if (r.ErrorCount != 0) {
return string.Format("{0} resolution/type errors detected in {1}", r.ErrorCount, program.Name);
}
return null; // success
}
// Lower-case file names before comparing them, since Windows uses case-insensitive file names
private class IncludeComparer : IComparer<Include> {
public int Compare(Include x, Include y) {
return x.fullPath.ToLower().CompareTo(y.fullPath.ToLower());
}
}
public static string ParseIncludes(ModuleDecl module, BuiltIns builtIns, List<string> excludeFiles, Errors errs) {
SortedSet<Include> includes = new SortedSet<Include>(new IncludeComparer());
foreach (string fileName in excludeFiles) {
includes.Add(new Include(null, fileName, Path.GetFullPath(fileName)));
}
bool newlyIncluded;
do {
newlyIncluded = false;
List<Include> newFilesToInclude = new List<Include>();
foreach (Include include in ((LiteralModuleDecl)module).ModuleDef.Includes) {
bool isNew = includes.Add(include);
if (isNew) {
newlyIncluded = true;
newFilesToInclude.Add(include);
}
}
foreach (Include include in newFilesToInclude) {
string ret = ParseFile(include.filename, include.tok, module, builtIns, errs, false);
if (ret != null) {
return ret;
}
}
} while (newlyIncluded);
return null; // Success
}
private static string ParseFile(string dafnyFileName, Bpl.IToken tok, ModuleDecl module, BuiltIns builtIns, Errors errs, bool verifyThisFile = true) {
var fn = DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(dafnyFileName) : dafnyFileName;
try {
int errorCount = Dafny.Parser.Parse(dafnyFileName, module, builtIns, errs, verifyThisFile);
if (errorCount != 0) {
return string.Format("{0} parse errors detected in {1}", errorCount, fn);
}
} catch (IOException e) {
errs.SemErr(tok, "Unable to open included file");
return string.Format("Error opening file \"{0}\": {1}", fn, e.Message);
}
return null; // Success
}
}
}
|
