From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/BoogieDriver/BoogieDriver.cs | 212 ++++++++++++++++++------------------ 1 file changed, 106 insertions(+), 106 deletions(-) (limited to 'Source/BoogieDriver/BoogieDriver.cs') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index fa038803..be88a745 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -1,106 +1,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 fileList = new List(); - 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; - } - } -} +//----------------------------------------------------------------------------- +// +// 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 fileList = new List(); + 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; + } + } +} -- cgit v1.2.3