From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: Normalise line endings using a .gitattributes file. Unfortunately this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. --- Source/BoogieDriver/BoogieDriver.cs | 212 +++++------ Source/BoogieDriver/BoogieDriver.csproj | 646 ++++++++++++++++---------------- Source/BoogieDriver/cce.cs | 210 +++++------ 3 files changed, 534 insertions(+), 534 deletions(-) (limited to 'Source/BoogieDriver') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index cba74bc5..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; + } + } +} diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index 14d607f9..90e0be41 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -1,324 +1,324 @@ - - - - Debug - AnyCPU - 9.0.21022 - 2.0 - {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A} - Exe - Properties - BoogieDriver - Boogie - v4.0 - 512 - 1 - true - ..\InterimKey.snk - - - 3.5 - - false - - publish\ - true - Disk - false - Foreground - 7 - Days - false - false - true - 0 - 1.0.0.%2a - false - true - - - true - full - false - ..\..\Binaries\ - TRACE;DEBUG - prompt - 4 - False - False - True - False - False - False - False - False - False - False - False - True - False - False - False - - - - - - - - - - - - - Full - %28none%29 - AllRules.ruleset - - - pdbonly - true - ..\..\Binaries\ - TRACE - prompt - 4 - AllRules.ruleset - - - true - ..\Provers\Z3api\bin\z3apidebug\ - DEBUG;TRACE - full - x86 - - - true - GlobalSuppressions.cs - prompt - Migrated rules for BoogieDriver.ruleset - true - 4 - false - - - true - ..\..\Binaries\ - DEBUG;TRACE - full - AnyCPU - ..\..\Binaries\Boogie.exe.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - AllRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - True - False - True - False - False - False - False - False - False - False - False - False - True - False - False - False - - - - - - - False - Full - Build - 0 - 4 - false - - - true - bin\x86\Debug\ - TRACE;DEBUG - full - x86 - ..\..\Binaries\Boogie.exe.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - AllRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - false - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - 4 - false - - - bin\x86\Release\ - TRACE - true - pdbonly - x86 - bin\Release\Boogie.exe.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - AllRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - false - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - false - 4 - - - true - bin\x86\z3apidebug\ - DEBUG;TRACE - full - x86 - bin\z3apidebug\Boogie.exe.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - Migrated rules for BoogieDriver.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - false - true - 4 - false - - - true - bin\x86\Checked\ - DEBUG;TRACE - full - x86 - ..\..\Binaries\Boogie.exe.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - AllRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - false - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - false - 4 - false - - - true - bin\QED\ - TRACE;DEBUG - full - AnyCPU - prompt - AllRules.ruleset - - - true - ..\..\Binaries\ - TRACE;DEBUG - full - AnyCPU - prompt - AllRules.ruleset - false - - - - - - - - - - - - - {0EFA3E43-690B-48DC-A72C-384A3EA7F31F} - AbsInt - - - {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} - Basetypes - - - {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} - CodeContractsExtender - - - {B230A69C-C466-4065-B9C1-84D80E76D802} - Core - - - {884386A3-58E9-40BB-A273-B24976775553} - Doomed - - - {EAA5EB79-D475-4601-A59B-825C191CD25F} - ExecutionEngine - - - {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} - Graph - - - {CF41E903-78EB-43BA-A355-E5FEB5ECECD4} - Houdini - - - {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} - ParserHelper - - - {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44} - Predication - - - {9B163AA3-36BC-4AFB-88AB-79BC9E97E401} - SMTLib - - - {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1} - VCExpr - - - {E1F10180-C7B9-4147-B51F-FA1B701966DC} - VCGeneration - - - - - - - - False - .NET Framework 3.5 SP1 Client Profile - false - - - False - .NET Framework 3.5 SP1 - true - - - False - Windows Installer 3.1 - true - - - - + + + + Debug + AnyCPU + 9.0.21022 + 2.0 + {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A} + Exe + Properties + BoogieDriver + Boogie + v4.0 + 512 + 1 + true + ..\InterimKey.snk + + + 3.5 + + false + + publish\ + true + Disk + false + Foreground + 7 + Days + false + false + true + 0 + 1.0.0.%2a + false + true + + + true + full + false + ..\..\Binaries\ + TRACE;DEBUG + prompt + 4 + False + False + True + False + False + False + False + False + False + False + False + True + False + False + False + + + + + + + + + + + + + Full + %28none%29 + AllRules.ruleset + + + pdbonly + true + ..\..\Binaries\ + TRACE + prompt + 4 + AllRules.ruleset + + + true + ..\Provers\Z3api\bin\z3apidebug\ + DEBUG;TRACE + full + x86 + + + true + GlobalSuppressions.cs + prompt + Migrated rules for BoogieDriver.ruleset + true + 4 + false + + + true + ..\..\Binaries\ + DEBUG;TRACE + full + AnyCPU + ..\..\Binaries\Boogie.exe.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + AllRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + True + False + True + False + False + False + False + False + False + False + False + False + True + False + False + False + + + + + + + False + Full + Build + 0 + 4 + false + + + true + bin\x86\Debug\ + TRACE;DEBUG + full + x86 + ..\..\Binaries\Boogie.exe.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + AllRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + false + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + 4 + false + + + bin\x86\Release\ + TRACE + true + pdbonly + x86 + bin\Release\Boogie.exe.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + AllRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + false + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + false + 4 + + + true + bin\x86\z3apidebug\ + DEBUG;TRACE + full + x86 + bin\z3apidebug\Boogie.exe.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + Migrated rules for BoogieDriver.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + false + true + 4 + false + + + true + bin\x86\Checked\ + DEBUG;TRACE + full + x86 + ..\..\Binaries\Boogie.exe.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + AllRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + false + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + false + 4 + false + + + true + bin\QED\ + TRACE;DEBUG + full + AnyCPU + prompt + AllRules.ruleset + + + true + ..\..\Binaries\ + TRACE;DEBUG + full + AnyCPU + prompt + AllRules.ruleset + false + + + + + + + + + + + + + {0EFA3E43-690B-48DC-A72C-384A3EA7F31F} + AbsInt + + + {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} + Basetypes + + + {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} + CodeContractsExtender + + + {B230A69C-C466-4065-B9C1-84D80E76D802} + Core + + + {884386A3-58E9-40BB-A273-B24976775553} + Doomed + + + {EAA5EB79-D475-4601-A59B-825C191CD25F} + ExecutionEngine + + + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} + Graph + + + {CF41E903-78EB-43BA-A355-E5FEB5ECECD4} + Houdini + + + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} + ParserHelper + + + {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44} + Predication + + + {9B163AA3-36BC-4AFB-88AB-79BC9E97E401} + SMTLib + + + {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1} + VCExpr + + + {E1F10180-C7B9-4147-B51F-FA1B701966DC} + VCGeneration + + + + + + + + False + .NET Framework 3.5 SP1 Client Profile + false + + + False + .NET Framework 3.5 SP1 + true + + + False + Windows Installer 3.1 + true + + + + \ No newline at end of file diff --git a/Source/BoogieDriver/cce.cs b/Source/BoogieDriver/cce.cs index 23d79815..42cabfcb 100644 --- a/Source/BoogieDriver/cce.cs +++ b/Source/BoogieDriver/cce.cs @@ -1,105 +1,105 @@ - -using System; -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using System.Text; -using Microsoft.Boogie; - - /// - /// A class containing static methods to extend the functionality of Code Contracts - /// - -public static class cce { - [Pure] - public static T NonNull(T t) { - Contract.Assert(t != null); - return t; - } - [Pure] - public static bool NonNullElements(IEnumerable collection) { - return collection != null && Contract.ForAll(collection, c => c != null); - } - [Pure] - public static bool NonNullElements(IDictionary collection) { - return collection != null && NonNullElements(collection.Keys) && NonNullElements(collection.Values); - } - [Pure] - public static bool NonNullElements(VariableSeq collection) { - return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); - } - [Pure] - public static void BeginExpose(object o) { - } - [Pure] - public static void EndExpose() { - } - [Pure] - public static bool IsPeerConsistent(object o) { - return true; - } - [Pure] - public static bool IsConsistent(object o) { - return true; - } - [Pure] - public static bool IsExposable(object o) { - return true; - } - [Pure] - public static bool IsExposed(object o) { - return true; - } - public static class Owner { - [Pure] - public static bool Same(object o, object p) { - return true; - } - [Pure] - public static void AssignSame(object o, object p) { - } - [Pure] - public static object ElementProxy(object o) { - return o; - } - [Pure] - public static bool None(object o) { - return true; - } - } - [Pure] - public static void LoopInvariant(bool p) { - Contract.Assert(p); - } - - public class UnreachableException : Exception { - public UnreachableException() { - } - } -} - -public class PeerAttribute : System.Attribute { -} -public class RepAttribute : System.Attribute { -} -public class CapturedAttribute : System.Attribute { -} -public class NotDelayedAttribute : System.Attribute { -} -public class NoDefaultContractAttribute : System.Attribute { -} -public class VerifyAttribute : System.Attribute { - public VerifyAttribute(bool b) { - - } -} -public class StrictReadonlyAttribute : System.Attribute { - } -public class AdditiveAttribute : System.Attribute { -} -public class ReadsAttribute : System.Attribute { - public enum Reads { - Nothing, - }; - public ReadsAttribute(object o) { - } -} + +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Text; +using Microsoft.Boogie; + + /// + /// A class containing static methods to extend the functionality of Code Contracts + /// + +public static class cce { + [Pure] + public static T NonNull(T t) { + Contract.Assert(t != null); + return t; + } + [Pure] + public static bool NonNullElements(IEnumerable collection) { + return collection != null && Contract.ForAll(collection, c => c != null); + } + [Pure] + public static bool NonNullElements(IDictionary collection) { + return collection != null && NonNullElements(collection.Keys) && NonNullElements(collection.Values); + } + [Pure] + public static bool NonNullElements(VariableSeq collection) { + return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); + } + [Pure] + public static void BeginExpose(object o) { + } + [Pure] + public static void EndExpose() { + } + [Pure] + public static bool IsPeerConsistent(object o) { + return true; + } + [Pure] + public static bool IsConsistent(object o) { + return true; + } + [Pure] + public static bool IsExposable(object o) { + return true; + } + [Pure] + public static bool IsExposed(object o) { + return true; + } + public static class Owner { + [Pure] + public static bool Same(object o, object p) { + return true; + } + [Pure] + public static void AssignSame(object o, object p) { + } + [Pure] + public static object ElementProxy(object o) { + return o; + } + [Pure] + public static bool None(object o) { + return true; + } + } + [Pure] + public static void LoopInvariant(bool p) { + Contract.Assert(p); + } + + public class UnreachableException : Exception { + public UnreachableException() { + } + } +} + +public class PeerAttribute : System.Attribute { +} +public class RepAttribute : System.Attribute { +} +public class CapturedAttribute : System.Attribute { +} +public class NotDelayedAttribute : System.Attribute { +} +public class NoDefaultContractAttribute : System.Attribute { +} +public class VerifyAttribute : System.Attribute { + public VerifyAttribute(bool b) { + + } +} +public class StrictReadonlyAttribute : System.Attribute { + } +public class AdditiveAttribute : System.Attribute { +} +public class ReadsAttribute : System.Attribute { + public enum Reads { + Nothing, + }; + public ReadsAttribute(object o) { + } +} -- cgit v1.2.3