blob: be88a7452668b0ac9ff880543647650b3a480507 (
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
|
//-----------------------------------------------------------------------------
//
// 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.Generic;
using System.Diagnostics.Contracts;
/*
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 int 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(Console.Out, "*** 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(Console.Out, "*** 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(Console.Out, "*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,
extension == null ? "" : extension);
goto END;
}
}
ExecutionEngine.ProcessFiles(fileList);
return 0;
END:
if (CommandLineOptions.Clo.XmlSink != null) {
CommandLineOptions.Clo.XmlSink.Close();
}
if (CommandLineOptions.Clo.Wait) {
Console.WriteLine("Press Enter to exit.");
Console.ReadLine();
}
return 1;
}
}
}
|
