blob: d35ac5f2c4e7d636ebe7e389110c100f776cb37e (
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
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
132
133
134
135
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
//---------------------------------------------------------------------------------------------
// OnlyBoogie OnlyBoogie.ssc
// - main program for taking a BPL program and verifying it
//---------------------------------------------------------------------------------------------
namespace Microsoft.Boogie {
using System;
using System.IO;
using System.Collections;
using System.Collections.Concurrent;
using System.Collections.Generic;
using PureCollections;
using Microsoft.Boogie;
using Microsoft.Boogie.AbstractInterpretation;
using System.Diagnostics.Contracts;
using System.Diagnostics;
using System.Linq;
using VC;
using BoogiePL = Microsoft.Boogie;
/*
The following assemblies are referenced because they are needed at runtime, not at compile time:
BaseTypes
Provers.Z3
System.Compiler.Framework
*/
public class OnlyBoogie
{
public static void Main(string[] args)
{
Contract.Requires(cce.NonNullElements(args));
ExecutionEngine.printer = new ConsolePrinter();
CommandLineOptions.Install(new CommandLineOptions());
CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;
if (!CommandLineOptions.Clo.Parse(args)) {
goto END;
}
if (CommandLineOptions.Clo.Files.Count == 0) {
ExecutionEngine.printer.ErrorWriteLine("*** Error: No input files were specified.");
goto END;
}
if (CommandLineOptions.Clo.XmlSink != null) {
string errMsg = CommandLineOptions.Clo.XmlSink.Open();
if (errMsg != null) {
ExecutionEngine.printer.ErrorWriteLine("*** Error: " + errMsg);
goto END;
}
}
if (!CommandLineOptions.Clo.DontShowLogo) {
Console.WriteLine(CommandLineOptions.Clo.Version);
}
if (CommandLineOptions.Clo.ShowEnv == CommandLineOptions.ShowEnvironment.Always) {
Console.WriteLine("---Command arguments");
foreach (string arg in args) {
Contract.Assert(arg != null);
Console.WriteLine(arg);
}
Console.WriteLine("--------------------");
}
Helpers.ExtraTraceInformation("Becoming sentient");
List<string> fileList = new List<string>();
foreach (string file in CommandLineOptions.Clo.Files) {
string extension = Path.GetExtension(file);
if (extension != null) {
extension = extension.ToLower();
}
if (extension == ".txt") {
StreamReader stream = new StreamReader(file);
string s = stream.ReadToEnd();
fileList.AddRange(s.Split(new char[3] {' ', '\n', '\r'}, StringSplitOptions.RemoveEmptyEntries));
}
else {
fileList.Add(file);
}
}
foreach (string file in fileList) {
Contract.Assert(file != null);
string extension = Path.GetExtension(file);
if (extension != null) {
extension = extension.ToLower();
}
if (extension != ".bpl") {
ExecutionEngine.printer.ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,
extension == null ? "" : extension);
goto END;
}
}
ExecutionEngine.ProcessFiles(fileList);
END:
if (CommandLineOptions.Clo.XmlSink != null) {
CommandLineOptions.Clo.XmlSink.Close();
}
if (CommandLineOptions.Clo.Wait) {
Console.WriteLine("Press Enter to exit.");
Console.ReadLine();
}
}
#region // TODO: Is this still used?
enum FileType
{
Unknown,
Cil,
Bpl,
Dafny
};
static bool ProgramHasDebugInfo(Program program)
{
Contract.Requires(program != null);
// We inspect the last declaration because the first comes from the prelude and therefore always has source context.
return program.TopLevelDeclarations.Count > 0 &&
((cce.NonNull(program.TopLevelDeclarations)[program.TopLevelDeclarations.Count - 1]).tok.IsValid);
}
#endregion
}
}
|
