blob: a7d863fea9db33ab0694773a2dbf036070610b3c (
plain)
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
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.IO;
using System.Collections.Generic;
using Microsoft.Contracts;
using Bpl = Microsoft.Boogie;
namespace Microsoft.Dafny {
public class Main {
/// <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.*;
{
program = null;
Dafny.Errors.count = 0;
List<ModuleDecl!> modules = new List<ModuleDecl!>();
foreach (string! dafnyFileName in fileNames){
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);
}
int errorCount;
try
{
errorCount = Dafny.Parser.Parse(dafnyFileName, modules);
if (errorCount != 0)
{
return string.Format("{0} parse errors detected in {1}", Dafny.Errors.count, dafnyFileName);
}
}
catch (IOException e)
{
return string.Format("Error opening file \"{0}\": {1}", dafnyFileName, e.Message);
}
}
program = new Program(programName, modules);
if (Bpl.CommandLineOptions.Clo.DafnyPrintFile != null) {
string filename = Bpl.CommandLineOptions.Clo.DafnyPrintFile;
if (filename == "-") {
Printer pr = new Printer(System.Console.Out);
pr.PrintProgram(program);
} else {
using (TextWriter writer = new System.IO.StreamWriter(filename)) {
Printer pr = new Printer(writer);
pr.PrintProgram(program);
}
}
}
if (Bpl.CommandLineOptions.Clo.NoResolve || Bpl.CommandLineOptions.Clo.NoTypecheck) { return null; }
Dafny.Resolver r = new Dafny.Resolver();
r.ResolveProgram(program);
if (r.ErrorCount != 0) {
return string.Format("{0} resolution/type errors detected in {1}", r.ErrorCount, programName);
}
return null; // success
}
}
}
|
