From 72b39a6962d7f6c7ca1aab9919791238c7baba3f Mon Sep 17 00:00:00 2001 From: tabarbe Date: Fri, 20 Aug 2010 22:32:24 +0000 Subject: Boogie: Committing changed source files --- Source/Core/CommandLineOptions.cs | 1276 +++++++++++++++++++++---------------- 1 file changed, 712 insertions(+), 564 deletions(-) (limited to 'Source/Core/CommandLineOptions.cs') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 6808be61..20a2fede 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -9,39 +9,75 @@ using System.Collections.Generic; using System.Collections.Specialized; using System.IO; using System.Diagnostics; -using Microsoft.Contracts; +using System.Diagnostics.Contracts; using Cci = System.Compiler; -namespace Microsoft.Boogie -{ - public class CommandLineOptions - { - public static string! VersionNumber { get { return (!)((!)System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location)).FileVersion; } } +namespace Microsoft.Boogie { + public class CommandLineOptions { + public static string/*!*/ VersionNumber { + get { + Contract.Ensures(Contract.Result() != null); + return cce.NonNull(cce.NonNull(System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location)).FileVersion); + } + } public const string ToolNameBoogie = "Boogie program verifier"; public const string ToolNameSpecSharp = "Spec# program verifier"; public const string ToolNameDafny = "Dafny program verifier"; - public static string! VersionSuffix { get { return " version " + VersionNumber + ", Copyright (c) 2003-2010, Microsoft."; } } - public string! InputFileExtension { - set - modifies _toolname, _version; - { + public static string/*!*/ VersionSuffix { + get { + Contract.Ensures(Contract.Result() != null); + return " version " + VersionNumber + ", Copyright (c) 2003-2010, Microsoft."; + } + } + public string/*!*/ InputFileExtension { + set { + Contract.Requires(value != null); + //modifies _toolname, _version; switch (value) { - case ".bpl": _toolname = ToolNameBoogie; break; - case ".dfy": _toolname = ToolNameDafny; break; - default: _toolname = ToolNameSpecSharp; break; + case ".bpl": + _toolname = ToolNameBoogie; + break; + case ".dfy": + _toolname = ToolNameDafny; + break; + default: + _toolname = ToolNameSpecSharp; + break; } _version = _toolname + VersionSuffix; } } - string! _toolname = ToolNameBoogie; - string! _version = ToolNameBoogie + VersionSuffix; - public string! ToolName { get { return _toolname; } } - public string! Version { get { return _version; } } - - public static CommandLineOptions! Clo = new CommandLineOptions(); // singleton to access all global data - - public string! Environment = ""; - public string! FileName = "unknown"; + string/*!*/ _toolname = ToolNameBoogie; + string/*!*/ _version = ToolNameBoogie + VersionSuffix; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(_toolname != null); + Contract.Invariant(_version != null); + Contract.Invariant(Clo != null); + Contract.Invariant(Environment != null); + Contract.Invariant(FileName != null); + Contract.Invariant(cce.NonNullElements(Files)); + Contract.Invariant(cce.NonNullElements(ContractAssemblies)); + Contract.Invariant(FileTimestamp != null); + } + + public string/*!*/ ToolName { + get { + Contract.Ensures(Contract.Result() != null); + return _toolname; + } + } + public string/*!*/ Version { + get { + Contract.Ensures(Contract.Result() != null); + return _version; + } + } + + public static CommandLineOptions/*!*/ Clo = new CommandLineOptions(); // singleton to access all global data + + public string/*!*/ Environment = ""; + public string/*!*/ FileName = "unknown"; public const long Megabyte = 1048576; @@ -49,37 +85,48 @@ namespace Microsoft.Boogie public bool RunningBoogieFromCommandLine = false; // "false" means running Boogie from the plug-in public bool RunningBoogieOnSsc = true; // "true" means running Boogie on ssc input while false means running it on bpl input - + public bool AttrHelpRequested = false; - - [Peer] public List! Files = new List(); - public List! ContractAssemblies = new List(); - - public string! FileTimestamp = ((!)DateTime.Now.ToString("o")).Replace(':', '.'); - public void ExpandFilename(ref string pattern) - { + + [Peer] + public List/*!*/ Files = new List(); + public List/*!*/ ContractAssemblies = new List(); + + public string/*!*/ FileTimestamp = cce.NonNull(DateTime.Now.ToString("o")).Replace(':', '.'); + public void ExpandFilename(ref string pattern) { if (pattern != null) { pattern = pattern.Replace("@PREFIX@", LogPrefix).Replace("@TIME@", FileTimestamp); - string fn = Files.Count == 0 ? "" : Files[Files.Count-1]; + string fn = Files.Count == 0 ? "" : Files[Files.Count - 1]; fn = fn.Replace('/', '-').Replace('\\', '-'); pattern = pattern.Replace("@FILE@", fn); } } + [ContractInvariantMethod] + void ObjectInvariant2() { + Contract.Invariant(LogPrefix != null); + Contract.Invariant(0 <= PrintUnstructured && PrintUnstructured < 3); // 0 = print only structured, 1 = both structured and unstructured, 2 = only unstructured + + } + public string PrintFile = null; public int PrintUnstructured = 0; - invariant 0 <= PrintUnstructured && PrintUnstructured < 3; // 0 = print only structured, 1 = both structured and unstructured, 2 = only unstructured + public bool PrintDesugarings = false; public string SimplifyLogFilePath = null; public string SMTLibOutputPath = "boogie-vc-@PROC@.smt"; - public string! LogPrefix = ""; + public string/*!*/ LogPrefix = ""; public bool PrintInstrumented = false; public bool InstrumentWithAsserts = false; - public enum InstrumentationPlaces { LoopHeaders, Everywhere } + public enum InstrumentationPlaces { + LoopHeaders, + Everywhere + } public InstrumentationPlaces InstrumentInfer = InstrumentationPlaces.LoopHeaders; public bool PrintWithUniqueASTIds = false; private string XmlSinkFilename = null; - [Peer] public XmlSink XmlSink = null; + [Peer] + public XmlSink XmlSink = null; public bool Wait = false; public bool Trace = false; public bool TraceTimes = false; @@ -94,93 +141,145 @@ namespace Microsoft.Boogie public bool UseUncheckedContracts = false; public bool SimplifyLogFileAppend = false; public bool SoundnessSmokeTest = false; - + private bool noConsistencyChecks = false; public bool NoConsistencyChecks { - get {return !Verify ? true : noConsistencyChecks;} + get { + return !Verify ? true : noConsistencyChecks; + } set - modifies noConsistencyChecks; - {noConsistencyChecks = value;} + //modifies noConsistencyChecks; + { + noConsistencyChecks = value; + } } public string DafnyPrintFile = null; public bool Compile = true; - - public enum ProverWarnings { None, Stdout, Stderr } + + public enum ProverWarnings { + None, + Stdout, + Stderr + } public ProverWarnings PrintProverWarnings = ProverWarnings.None; public int ProverShutdownLimit = 0; - - public enum SubsumptionOption { Never, NotForQuantifiers, Always } + + public enum SubsumptionOption { + Never, + NotForQuantifiers, + Always + } public SubsumptionOption UseSubsumption = SubsumptionOption.Always; public bool AlwaysAssumeFreeLoopInvariants = false; - public enum ShowEnvironment { Never, DuringPrint, Always } + public enum ShowEnvironment { + Never, + DuringPrint, + Always + } public ShowEnvironment ShowEnv = ShowEnvironment.DuringPrint; public bool DontShowLogo = false; - + [ContractInvariantMethod] + void ObjectInvariant3() { + Contract.Invariant(0 <= CheckingLevel && CheckingLevel < 3); + Contract.Invariant(0 <= OrderStrength && OrderStrength < 2); + Contract.Invariant(0 <= SummationAxiomStrength && SummationAxiomStrength < 2); + Contract.Invariant(0 <= InductiveMinMax && InductiveMinMax < 6); + Contract.Invariant(0 <= FCOStrength && FCOStrength < 6); + Contract.Invariant(-1 <= LoopFrameConditions && LoopFrameConditions < 3); + Contract.Invariant(0 <= ModifiesDefault && ModifiesDefault < 7); + Contract.Invariant((0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4); + Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2); + Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9); + Contract.Invariant(-1 <= BracketIdsInVC && BracketIdsInVC <= 1); + Contract.Invariant(cce.NonNullElements(ProverOptions)); + + + + + + + } + public int CheckingLevel = 2; - invariant 0 <= CheckingLevel && CheckingLevel < 3; - public enum Methodology { Boogie, VisibleState } + public enum Methodology { + Boogie, + VisibleState + } public Methodology MethodologySelection = Methodology.Boogie; public int OrderStrength = 0; - invariant 0 <= OrderStrength && OrderStrength < 2; public bool UseArithDistributionAxioms = false; public int SummationAxiomStrength = 1; - invariant 0 <= SummationAxiomStrength && SummationAxiomStrength < 2; public int InductiveMinMax = 0; - invariant 0 <= InductiveMinMax && InductiveMinMax < 6; public int FCOStrength = 5; - invariant 0 <= FCOStrength && FCOStrength < 6; public int LoopUnrollCount = -1; // -1 means don't unroll loops public int LoopFrameConditions = -1; // -1 means not specified -- this will be replaced by the "implications" section below - invariant -1 <= LoopFrameConditions && LoopFrameConditions < 3; public int ModifiesDefault = 5; - invariant 0 <= ModifiesDefault && ModifiesDefault < 7; public bool LocalModifiesChecks = true; public bool NoVerifyByDefault = false; - public enum OwnershipModelOption { Standard, Experimental, Trivial } + public enum OwnershipModelOption { + Standard, + Experimental, + Trivial + } public OwnershipModelOption OwnershipModelEncoding = OwnershipModelOption.Standard; public int PrintErrorModel = 0; public string PrintErrorModelFile = null; - invariant (0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4; public bool CEVPrint = false; public int EnhancedErrorMessages = 0; - invariant 0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2; public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present - - public enum BvHandling { None, Z3Native, ToInt } + public enum BvHandling { + None, + Z3Native, + ToInt + } public BvHandling Bitvectors = BvHandling.Z3Native; - public bool UseArrayTheory = false; - public bool MonomorphicArrays { get { return UseArrayTheory || TypeEncodingMethod == TypeEncoding.Monomorphic; } } + public bool MonomorphicArrays { + get { + return UseArrayTheory || TypeEncodingMethod == TypeEncoding.Monomorphic; + } + } public bool ExpandLambdas = true; // not useful from command line, only to be set to false programatically - - public bool DoModSetAnalysis = false; + public bool DoModSetAnalysis = false; public bool UseAbstractInterpretation = true; // true iff the user want to use abstract interpretation public int /*0..9*/StepsBeforeWidening = 0; // The number of steps that must be done before applying a widen operator - invariant 0 <= StepsBeforeWidening && StepsBeforeWidening <= 9; - public enum VCVariety { Structured, Block, Local, BlockNested, BlockReach, BlockNestedReach, Dag, Doomed, Unspecified } + + public enum VCVariety { + Structured, + Block, + Local, + BlockNested, + BlockReach, + BlockNestedReach, + Dag, + Doomed, + Unspecified + } public VCVariety vcVariety = VCVariety.Unspecified; // will not be Unspecified after command line has been parsed public bool useDoomDebug = false; // Will use doomed analysis to search for errors if set - + public bool RemoveEmptyBlocks = true; - public bool CoalesceBlocks = true; - - [Rep] public ProverFactory TheProverFactory; + public bool CoalesceBlocks = true; + + [Rep] + public ProverFactory TheProverFactory; public string ProverName; - [Peer] public List! ProverOptions = new List(); + [Peer] + public List/*!*/ ProverOptions = new List(); public int BracketIdsInVC = -1; // -1 - not specified, 0 - no, 1 - yes public bool CausalImplies = false; - invariant -1 <= BracketIdsInVC && BracketIdsInVC <= 1; + public int SimplifyProverMatchDepth = -1; // -1 means not specified public int ProverKillTime = -1; // -1 means not specified public int SmokeTimeout = 10; // default to 10s public int ProverCCLimit = 5; public bool z3AtFlag = true; - public bool RestartProverPerVC = false; + public bool RestartProverPerVC = false; public double VcsMaxCost = 1.0; public double VcsPathJoinMult = 0.8; @@ -196,16 +295,26 @@ namespace Microsoft.Boogie public bool houdiniEnabled = false; public bool DebugRefuted = false; - - public XmlSink XmlRefuted - { - get { if (DebugRefuted) return XmlSink; else return null; } + + public XmlSink XmlRefuted { + get { + if (DebugRefuted) + return XmlSink; + else + return null; + } } - - [Peer] public List! Z3Options = new List(); + [ContractInvariantMethod] + void ObjectInvariant4() { + Contract.Invariant(cce.NonNullElements(Z3Options)); + Contract.Invariant(0 <= Z3lets && Z3lets < 4); + } + + [Peer] + public List/*!*/ Z3Options = new List(); public bool Z3types = false; public int Z3lets = 3; // 0 - none, 1 - only LET TERM, 2 - only LET FORMULA, 3 - (default) any - invariant 0 <= Z3lets && Z3lets < 4; + // Maximum amount of virtual memory (in bytes) for the prover to use // @@ -215,13 +324,24 @@ namespace Microsoft.Boogie // Minimum number of prover calls before restart public int MinNumOfProverCalls = 5; - public enum PlatformType{notSpecified, v1, v11, v2, cli1} + public enum PlatformType { + notSpecified, + v1, + v11, + v2, + cli1 + } public PlatformType TargetPlatform; public string TargetPlatformLocation; public string StandardLibraryLocation; - + // whether procedure inlining is enabled at call sites. - public enum Inlining { None, Assert, Assume, Spec }; + public enum Inlining { + None, + Assert, + Assume, + Spec + }; public Inlining ProcedureInlining = Inlining.Assume; public bool PrintInlined = false; public bool ExtractLoops = false; @@ -230,44 +350,69 @@ namespace Microsoft.Boogie public int StratifiedInliningOption = 0; public int RecursionBound = 500; public string CoverageReporterPath = null; - - public enum TypeEncoding { None, Predicates, Arguments, Monomorphic }; + + public enum TypeEncoding { + None, + Predicates, + Arguments, + Monomorphic + }; public TypeEncoding TypeEncodingMethod = TypeEncoding.Predicates; public bool Monomorphize = false; - + public bool ReflectAdd = false; public int LiveVariableAnalysis = 1; - + // Static constructor - static CommandLineOptions() - { + static CommandLineOptions() { if (System.Type.GetType("Mono.Runtime") == null) { // MONO - TraceListenerCollection! dbl = Debug.Listeners; - assume dbl.IsPeerConsistent; // hangs off static field + TraceListenerCollection/*!*/ dbl = Debug.Listeners; + Contract.Assert(dbl != null); + Contract.Assume(cce.IsPeerConsistent(dbl)); // hangs off static field #if WHIDBEY dbl.Add(new ConsoleTraceListener()); #else - dpl.Add(new DefaultTraceListener()); + dbl.Add(new DefaultTraceListener()); #endif } } private string methodToLog = null; private string methodToBreakOn = null; - - [Rep] private List procsToCheck = null; // null means "no restriction" - [Rep] private List methodsToTranslateSubstring = null; // null means "no restriction" - [Rep] private List methodsToTranslateMethod = null; // null means "no restriction" - [Rep] private List methodsToTranslateMethodQualified = null; // null means "no restriction" - [Rep] private List methodsToTranslateClass = null; // null means "no restriction" - [Rep] private List methodsToTranslateClassQualified = null; // null means "no restriction" - [Rep] private List methodsToTranslateFile = null; // null means "no restriction" - [Rep] private List! methodsToTranslateExclude = new List(); - - public class AiFlags - { + [ContractInvariantMethod] + void ObjectInvariant5() { + Contract.Invariant(cce.NonNullElements(procsToCheck, true)); + Contract.Invariant(cce.NonNullElements(methodsToTranslateClass, true)); + Contract.Invariant(cce.NonNullElements(methodsToTranslateClassQualified, true)); + Contract.Invariant(cce.NonNullElements(methodsToTranslateExclude)); + Contract.Invariant(cce.NonNullElements(methodsToTranslateFile, true)); + Contract.Invariant(cce.NonNullElements(methodsToTranslateMethod, true)); + Contract.Invariant(cce.NonNullElements(methodsToTranslateMethodQualified, true)); + Contract.Invariant(cce.NonNullElements(methodsToTranslateSubstring, true)); + Contract.Invariant(Ai != null); + Contract.Invariant(houdiniFlags != null); + } + + [Rep] + private List procsToCheck = null; // null means "no restriction" + [Rep] + private List methodsToTranslateSubstring = null; // null means "no restriction" + [Rep] + private List methodsToTranslateMethod = null; // null means "no restriction" + [Rep] + private List methodsToTranslateMethodQualified = null; // null means "no restriction" + [Rep] + private List methodsToTranslateClass = null; // null means "no restriction" + [Rep] + private List methodsToTranslateClassQualified = null; // null means "no restriction" + [Rep] + private List methodsToTranslateFile = null; // null means "no restriction" + [Rep] + private List/*!*/ methodsToTranslateExclude = new List(); + + public class AiFlags { public bool Intervals = false; public bool Constant = false; public bool DynamicType = false; @@ -275,26 +420,24 @@ namespace Microsoft.Boogie public bool Polyhedra = false; public bool DebugStatistics = false; - public bool AnySet - { - get - { - return Intervals - || Constant - || DynamicType - || Nullness - || Polyhedra; - } - } + public bool AnySet { + get { + return Intervals + || Constant + || DynamicType + || Nullness + || Polyhedra; + } + } } - public AiFlags! Ai = new AiFlags(); + public AiFlags/*!*/ Ai = new AiFlags(); public class HoudiniFlags { public bool continueAtError = false; public bool incremental = false; } - - public HoudiniFlags! houdiniFlags = new HoudiniFlags(); + + public HoudiniFlags/*!*/ houdiniFlags = new HoudiniFlags(); [Verify(false)] public CommandLineOptions() { @@ -312,47 +455,44 @@ namespace Microsoft.Boogie /// /// Consumed ("captured" and possibly modified) by the method. [Verify(false)] - public int Parse([Captured] string[]! args) - requires forall{int i in (0:args.Length); args[i] != null}; - ensures TheProverFactory != null; - ensures vcVariety != VCVariety.Unspecified; - ensures -2 <= result && result <= 2 && result != 0; - { + public int Parse([Captured] string[]/*!*/ args) { + Contract.Requires(cce.NonNullElements(args)); + Contract.Ensures(TheProverFactory != null); + Contract.Ensures(vcVariety != VCVariety.Unspecified); + Contract.Ensures(-2 <= Contract.Result() && Contract.Result() <= 2 && Contract.Result() != 0); // save the command line options for the log files Environment += "Command Line Options:"; foreach (string s in args) - Environment += " " + s; - args = (string[]!)args.Clone(); // the operations performed may mutate the array, so make a copy - CommandLineParseState! ps = new CommandLineParseState(args); + Environment += " " + s; + args = cce.NonNull((string[])args.Clone()); // the operations performed may mutate the array, so make a copy + CommandLineParseState/*!*/ ps = new CommandLineParseState(args); + Contract.Assert(ps != null); int res = 1; // the result value - - while (ps.i < args.Length) - invariant ps.IsPeerConsistent; - invariant ps.args == args; - { + + while (ps.i < args.Length) { + cce.LoopInvariant(cce.IsPeerConsistent(ps)); + cce.LoopInvariant(ps.args == args); ps.s = args[ps.i]; - assert ps.s != null; + Contract.Assert(ps.s != null); ps.s = ps.s.Trim(); int colonIndex = ps.s.IndexOf(':'); - if (colonIndex >= 0 && (ps.s.StartsWith("-") || ps.s.StartsWith("/"))) - { + if (colonIndex >= 0 && (ps.s.StartsWith("-") || ps.s.StartsWith("/"))) { ps.hasColonArgument = true; - args[ps.i] = ps.s.Substring(colonIndex+1); + args[ps.i] = ps.s.Substring(colonIndex + 1); ps.s = ps.s.Substring(0, colonIndex); - } - else - { - expose(ps) { + } else { + cce.BeginExpose(ps); + { ps.i++; } + cce.EndExpose(); ps.hasColonArgument = false; - } + } ps.nextIndex = ps.i; - switch (ps.s) - { + switch (ps.s) { case "-help": case "/help": case "-?": @@ -368,31 +508,48 @@ namespace Microsoft.Boogie AttrHelpRequested = true; } break; - + case "-infer": case "/infer": - if (ps.ConfirmArgumentCount(1)) { - foreach (char c in (!)args[ps.i]) - { - switch (c) - { - case 'i': Ai.Intervals = true; UseAbstractInterpretation = true; break; - case 'c': Ai.Constant = true; UseAbstractInterpretation = true; break; - case 'd': Ai.DynamicType = true; UseAbstractInterpretation = true; break; - case 'n': Ai.Nullness = true; UseAbstractInterpretation = true; break; - case 'p': Ai.Polyhedra = true; UseAbstractInterpretation = true; break; - case 's': Ai.DebugStatistics = true; UseAbstractInterpretation = true; break; - case '0': - case '1': - case '2': - case '3': - case '4': - case '5': - case '6': - case '7': - case '8': + if (ps.ConfirmArgumentCount(1)) { + foreach (char c in cce.NonNull(args[ps.i])) { + switch (c) { + case 'i': + Ai.Intervals = true; + UseAbstractInterpretation = true; + break; + case 'c': + Ai.Constant = true; + UseAbstractInterpretation = true; + break; + case 'd': + Ai.DynamicType = true; + UseAbstractInterpretation = true; + break; + case 'n': + Ai.Nullness = true; + UseAbstractInterpretation = true; + break; + case 'p': + Ai.Polyhedra = true; + UseAbstractInterpretation = true; + break; + case 's': + Ai.DebugStatistics = true; + UseAbstractInterpretation = true; + break; + case '0': + case '1': + case '2': + case '3': + case '4': + case '5': + case '6': + case '7': + case '8': case '9': - StepsBeforeWidening = (int) char.GetNumericValue(c); break; + StepsBeforeWidening = (int)char.GetNumericValue(c); + break; default: ps.Error("Invalid argument '{0}' to option {1}", c.ToString(), ps.s); break; @@ -400,7 +557,7 @@ namespace Microsoft.Boogie } } break; - + case "-noinfer": case "/noinfer": if (ps.ConfirmArgumentCount(0)) { @@ -408,8 +565,8 @@ namespace Microsoft.Boogie } break; - case "-log": - case "/log": + case "-log": + case "/log": if (ps.hasColonArgument) { methodToLog = args[ps.i]; ps.nextIndex = ps.i + 1; @@ -417,62 +574,59 @@ namespace Microsoft.Boogie methodToLog = "*"; } break; - - case "-logInfer": - case "/logInfer": - Microsoft.AbstractInterpretationFramework.Lattice.LogSwitch = true; - break; - - case "-break": - case "/break": - if (ps.hasColonArgument) - { - methodToBreakOn = args[ps.i]; - ps.nextIndex = ps.i + 1; - } - else - { - System.Diagnostics.Debugger.Break(); + + case "-logInfer": + case "/logInfer": + Microsoft.AbstractInterpretationFramework.Lattice.LogSwitch = true; + break; + + case "-break": + case "/break": + if (ps.hasColonArgument) { + methodToBreakOn = args[ps.i]; + ps.nextIndex = ps.i + 1; + } else { + System.Diagnostics.Debugger.Break(); } break; - - case "-launch": - case "/launch": - System.Diagnostics.Debugger.Launch(); - break; - + + case "-launch": + case "/launch": + System.Diagnostics.Debugger.Launch(); + break; + case "-proc": case "/proc": if (procsToCheck == null) { - procsToCheck = new List(); + procsToCheck = new List(); } if (ps.ConfirmArgumentCount(1)) { - procsToCheck.Add((!)args[ps.i]); + procsToCheck.Add(cce.NonNull(args[ps.i])); } break; case "-translate": case "/translate": if (methodsToTranslateSubstring == null) { - methodsToTranslateSubstring = new List(); + methodsToTranslateSubstring = new List(); } if (ps.ConfirmArgumentCount(1)) { - methodsToTranslateSubstring.Add((!)args[ps.i]); + methodsToTranslateSubstring.Add(cce.NonNull(args[ps.i])); } break; case "-trMethod": case "/trMethod": if (ps.ConfirmArgumentCount(1)) { - string m = (!)args[ps.i]; + string m = cce.NonNull(args[ps.i]); if (0 <= m.IndexOf('.')) { if (methodsToTranslateMethodQualified == null) { - methodsToTranslateMethodQualified = new List(); + methodsToTranslateMethodQualified = new List(); } methodsToTranslateMethodQualified.Add(m); } else { if (methodsToTranslateMethod == null) { - methodsToTranslateMethod = new List(); + methodsToTranslateMethod = new List(); } methodsToTranslateMethod.Add(m); } @@ -482,15 +636,15 @@ namespace Microsoft.Boogie case "-trClass": case "/trClass": if (ps.ConfirmArgumentCount(1)) { - string m = (!)args[ps.i]; + string m = cce.NonNull(args[ps.i]); if (0 <= m.IndexOf('.')) { if (methodsToTranslateClassQualified == null) { - methodsToTranslateClassQualified = new List(); + methodsToTranslateClassQualified = new List(); } methodsToTranslateClassQualified.Add(m); } else { if (methodsToTranslateClass == null) { - methodsToTranslateClass = new List(); + methodsToTranslateClass = new List(); } methodsToTranslateClass.Add(m); } @@ -500,109 +654,100 @@ namespace Microsoft.Boogie case "-trFile": case "/trFile": if (methodsToTranslateFile == null) { - methodsToTranslateFile = new List(); + methodsToTranslateFile = new List(); } if (ps.ConfirmArgumentCount(1)) { - methodsToTranslateFile.Add((!)args[ps.i]); + methodsToTranslateFile.Add(cce.NonNull(args[ps.i])); } break; case "-trExclude": case "/trExclude": if (ps.ConfirmArgumentCount(1)) { - methodsToTranslateExclude.Add((!)args[ps.i]); + methodsToTranslateExclude.Add(cce.NonNull(args[ps.i])); } break; case "-xml": case "/xml": - if (ps.ConfirmArgumentCount(1)) - { + if (ps.ConfirmArgumentCount(1)) { XmlSinkFilename = args[ps.i]; } - break; - + break; + case "-print": case "/print": - if (ps.ConfirmArgumentCount(1)) - { + if (ps.ConfirmArgumentCount(1)) { PrintFile = args[ps.i]; } break; - + case "-dprint": case "/dprint": - if (ps.ConfirmArgumentCount(1)) - { + if (ps.ConfirmArgumentCount(1)) { DafnyPrintFile = args[ps.i]; } break; - + case "-compile": case "/compile": { - int compile = 0; - if (ps.GetNumericArgument(ref compile, 2)) { - Compile = compile == 1; + int compile = 0; + if (ps.GetNumericArgument(ref compile, 2)) { + Compile = compile == 1; + } + break; } - break; - } case "-contracts": case "/contracts": case "-c": case "/c": - if (ps.ConfirmArgumentCount(1)) - { - ContractAssemblies.Add((!)args[ps.i]); + if (ps.ConfirmArgumentCount(1)) { + ContractAssemblies.Add(cce.NonNull(args[ps.i])); } break; - + case "-proverLog": case "/proverLog": - if (ps.ConfirmArgumentCount(1)) - { + if (ps.ConfirmArgumentCount(1)) { SimplifyLogFilePath = args[ps.i]; } break; - + case "-logPrefix": case "/logPrefix": - if (ps.ConfirmArgumentCount(1)) - { - string s = (!)args[ps.i]; + if (ps.ConfirmArgumentCount(1)) { + string s = cce.NonNull(args[ps.i]); LogPrefix += s.Replace('/', '-').Replace('\\', '-'); } break; - + case "-proverShutdownLimit": case "/proverShutdownLimit": ps.GetNumericArgument(ref ProverShutdownLimit); break; - + case "-smtOutput": case "/smtOutput": - if (ps.ConfirmArgumentCount(1)) - { + if (ps.ConfirmArgumentCount(1)) { SMTLibOutputPath = args[ps.i]; } break; - + case "-errorTrace": case "/errorTrace": ps.GetNumericArgument(ref ErrorTrace, 3); break; - + case "-level": case "/level": ps.GetNumericArgument(ref CheckingLevel, 3); break; - + case "-methodology": case "/methodology": - if (ps.ConfirmArgumentCount(1)) - { - switch (args[ps.i]) - { + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) { case "b": case "Boogie": case "boogie": @@ -618,67 +763,70 @@ namespace Microsoft.Boogie } } break; - + case "-proverWarnings": case "/proverWarnings": { - int pw = 0; - if (ps.GetNumericArgument(ref pw, 3)) { - switch (pw) { - case 0: - PrintProverWarnings = ProverWarnings.None; - break; - case 1: - PrintProverWarnings = ProverWarnings.Stdout; - break; - case 2: - PrintProverWarnings = ProverWarnings.Stderr; - break; - default: - assert false; // postcondition of GetNumericArgument guarantees that we don't get here + int pw = 0; + if (ps.GetNumericArgument(ref pw, 3)) { + switch (pw) { + case 0: + PrintProverWarnings = ProverWarnings.None; + break; + case 1: + PrintProverWarnings = ProverWarnings.Stdout; + break; + case 2: + PrintProverWarnings = ProverWarnings.Stderr; + break; + default: { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // postcondition of GetNumericArgument guarantees that we don't get here + } } + break; } - break; - } case "-env": case "/env": { - int e = 0; - if (ps.GetNumericArgument(ref e, 3)) { - switch (e) { - case 0: - ShowEnv = ShowEnvironment.Never; - break; - case 1: - ShowEnv = ShowEnvironment.DuringPrint; - break; - case 2: - ShowEnv = ShowEnvironment.Always; - break; - default: - assert false; // postcondition of GetNumericArgument guarantees that we don't get here + int e = 0; + if (ps.GetNumericArgument(ref e, 3)) { + switch (e) { + case 0: + ShowEnv = ShowEnvironment.Never; + break; + case 1: + ShowEnv = ShowEnvironment.DuringPrint; + break; + case 2: + ShowEnv = ShowEnvironment.Always; + break; + default: { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // postcondition of GetNumericArgument guarantees that we don't get here + } } + break; } - break; - } case "-loopUnroll": case "/loopUnroll": ps.GetNumericArgument(ref LoopUnrollCount); break; - + case "-modifiesOnLoop": case "/modifiesOnLoop": ps.GetNumericArgument(ref LoopFrameConditions, 3); break; - + case "-modifiesDefault": case "/modifiesDefault": ps.GetNumericArgument(ref ModifiesDefault, 7); break; - + case "-localModifiesChecks": - case "/localModifiesChecks": - { + case "/localModifiesChecks": { int localChecks = 0; ps.GetNumericArgument(ref localChecks, 2); LocalModifiesChecks = (localChecks != 0); @@ -689,7 +837,7 @@ namespace Microsoft.Boogie case "/orderStrength": ps.GetNumericArgument(ref OrderStrength, 2); break; - + case "-summationStrength": case "/summationStrength": ps.GetNumericArgument(ref SummationAxiomStrength, 2); @@ -704,13 +852,11 @@ namespace Microsoft.Boogie case "/fcoStrength": ps.GetNumericArgument(ref FCOStrength, 6); break; - + case "-ownerModelEncoding": case "/ownerModelEncoding": - if (ps.ConfirmArgumentCount(1)) - { - switch (args[ps.i]) - { + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) { case "s": case "standard": OwnershipModelEncoding = OwnershipModelOption.Standard; @@ -729,13 +875,11 @@ namespace Microsoft.Boogie } } break; - + case "-printModel": case "/printModel": - if (ps.ConfirmArgumentCount(1)) - { - switch (args[ps.i]) - { + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) { case "0": PrintErrorModel = 0; break; @@ -755,46 +899,42 @@ namespace Microsoft.Boogie } break; - + case "-cev": case "/cev": - if (ps.ConfirmArgumentCount(1)) - { + if (ps.ConfirmArgumentCount(1)) { PrintErrorModelFile = args[ps.i]; } CEVPrint = true; - break; + break; case "-printModelToFile": case "/printModelToFile": - if (ps.ConfirmArgumentCount(1)) - { + if (ps.ConfirmArgumentCount(1)) { PrintErrorModelFile = args[ps.i]; } - break; + break; + - case "-enhancedErrorMessages": case "/enhancedErrorMessages": ps.GetNumericArgument(ref EnhancedErrorMessages, 2); break; - + case "-forceBplErrors": case "/forceBplErrors": ForceBplErrors = true; - break; - + break; + case "-bv": case "/bv": - if (ps.ConfirmArgumentCount(1)) - { + if (ps.ConfirmArgumentCount(1)) { if (TheProverFactory == null) { TheProverFactory = ProverFactory.Load("Z3"); ProverName = "Z3".ToUpper(); } - switch (args[ps.i]) - { + switch (args[ps.i]) { case "n": Bitvectors = BvHandling.None; break; @@ -810,72 +950,73 @@ namespace Microsoft.Boogie } } break; - + case "-contractInfer": case "/contractInfer": ContractInfer = true; TheProverFactory = ProverFactory.Load("ContractInference"); ProverName = "ContractInference".ToUpper(); break; - + case "-subsumption": case "/subsumption": { - int s = 0; - if (ps.GetNumericArgument(ref s, 3)) { - switch (s) { - case 0: - UseSubsumption = SubsumptionOption.Never; - break; - case 1: - UseSubsumption = SubsumptionOption.NotForQuantifiers; - break; - case 2: - UseSubsumption = SubsumptionOption.Always; - break; - default: - assert false; // postcondition of GetNumericArgument guarantees that we don't get here + int s = 0; + if (ps.GetNumericArgument(ref s, 3)) { + switch (s) { + case 0: + UseSubsumption = SubsumptionOption.Never; + break; + case 1: + UseSubsumption = SubsumptionOption.NotForQuantifiers; + break; + case 2: + UseSubsumption = SubsumptionOption.Always; + break; + default: { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // postcondition of GetNumericArgument guarantees that we don't get here + } } + break; } - break; - } - + case "-liveVariableAnalysis": case "/liveVariableAnalysis": { - int lva = 0; - if (ps.GetNumericArgument(ref lva, 3)) { - LiveVariableAnalysis = lva; + int lva = 0; + if (ps.GetNumericArgument(ref lva, 3)) { + LiveVariableAnalysis = lva; + } + break; } - break; - } - + case "-removeEmptyBlocks": case "/removeEmptyBlocks": { - int reb = 0; - if (ps.GetNumericArgument(ref reb, 2)) { - RemoveEmptyBlocks = reb == 1; + int reb = 0; + if (ps.GetNumericArgument(ref reb, 2)) { + RemoveEmptyBlocks = reb == 1; + } + break; } - break; - } - + case "-coalesceBlocks": case "/coalesceBlocks": { - int cb = 0; - if (ps.GetNumericArgument(ref cb, 2)) { - CoalesceBlocks = cb == 1; + int cb = 0; + if (ps.GetNumericArgument(ref cb, 2)) { + CoalesceBlocks = cb == 1; + } + break; } - break; - } case "/DoomDebug": vcVariety = VCVariety.Doomed; useDoomDebug = true; break; - + case "-vc": case "/vc": if (ps.ConfirmArgumentCount(1)) { - switch (args[ps.i]) - { + switch (args[ps.i]) { case "s": case "structured": vcVariety = VCVariety.Structured; @@ -915,15 +1056,15 @@ namespace Microsoft.Boogie case "-prover": case "/prover": if (ps.ConfirmArgumentCount(1)) { - TheProverFactory = ProverFactory.Load((!)args[ps.i]); - ProverName = ((!)args[ps.i]).ToUpper(); + TheProverFactory = ProverFactory.Load(cce.NonNull(args[ps.i])); + ProverName = cce.NonNull(args[ps.i]).ToUpper(); } break; case "-proverOpt": case "/proverOpt": if (ps.ConfirmArgumentCount(1)) { - ProverOptions.Add((!)args[ps.i]); + ProverOptions.Add(cce.NonNull(args[ps.i])); } break; @@ -936,8 +1077,7 @@ namespace Microsoft.Boogie case "-inline": case "/inline": if (ps.ConfirmArgumentCount(1)) { - switch (args[ps.i]) - { + switch (args[ps.i]) { case "none": ProcedureInlining = Inlining.None; break; @@ -959,13 +1099,12 @@ namespace Microsoft.Boogie case "-lazyInline": case "/lazyInline": if (ps.ConfirmArgumentCount(1)) { - switch (args[ps.i]) - { + switch (args[ps.i]) { case "0": - LazyInlining = 0; + LazyInlining = 0; break; case "1": - LazyInlining = 1; + LazyInlining = 1; break; case "2": LazyInlining = 2; @@ -979,44 +1118,42 @@ namespace Microsoft.Boogie case "-stratifiedInline": case "/stratifiedInline": if (ps.ConfirmArgumentCount(1)) { - switch (args[ps.i]) - { + switch (args[ps.i]) { case "0": - StratifiedInlining = 0; + StratifiedInlining = 0; break; case "1": - StratifiedInlining = 1; + StratifiedInlining = 1; break; default: - StratifiedInlining = Int32.Parse((!)args[ps.i]); + StratifiedInlining = Int32.Parse(cce.NonNull(args[ps.i])); //ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); break; } } - break; + break; case "-recursionBound": - case "/recursionBound": - if (ps.ConfirmArgumentCount(1)) { - RecursionBound = Int32.Parse((!)args[ps.i]); + case "/recursionBound": + if(ps.ConfirmArgumentCount(1)){ + RecursionBound = Int32.Parse(cce.NonNull(args[ps.i])); } - break; + break; case "-coverageReporter": case "/coverageReporter": if (ps.ConfirmArgumentCount(1)) { CoverageReporterPath = args[ps.i]; } - break; - case "-stratifiedInlineOption": + break; + case "-stratifiedInilneOption": case "/stratifiedInlineOption": if (ps.ConfirmArgumentCount(1)) { - StratifiedInliningOption = Int32.Parse((!)args[ps.i]); + StratifiedInliningOption=Int32.Parse(cce.NonNull(args[ps.i])); } - break; + break; case "-typeEncoding": case "/typeEncoding": if (ps.ConfirmArgumentCount(1)) { - switch (args[ps.i]) - { + switch (args[ps.i]) { case "n": case "none": TypeEncodingMethod = TypeEncoding.None; @@ -1043,8 +1180,7 @@ namespace Microsoft.Boogie case "-instrumentInfer": case "/instrumentInfer": if (ps.ConfirmArgumentCount(1)) { - switch (args[ps.i]) - { + switch (args[ps.i]) { case "e": InstrumentInfer = InstrumentationPlaces.Everywhere; break; @@ -1064,14 +1200,13 @@ namespace Microsoft.Boogie break; case "-proverMemoryLimit": - case "/proverMemoryLimit": - { - int d = 0; - if (ps.GetNumericArgument(ref d)) { - MaxProverMemory = d * Megabyte; + case "/proverMemoryLimit": { + int d = 0; + if (ps.GetNumericArgument(ref d)) { + MaxProverMemory = d * Megabyte; + } + break; } - break; - } case "-vcsMaxCost": case "/vcsMaxCost": @@ -1127,7 +1262,7 @@ namespace Microsoft.Boogie case "/simplifyMatchDepth": ps.GetNumericArgument(ref SimplifyProverMatchDepth); break; - + case "-timeLimit": case "/timeLimit": ps.GetNumericArgument(ref ProverKillTime); @@ -1137,17 +1272,16 @@ namespace Microsoft.Boogie case "/smokeTimeout": ps.GetNumericArgument(ref SmokeTimeout); break; - + case "-errorLimit": case "/errorLimit": ps.GetNumericArgument(ref ProverCCLimit); break; - + case "-z3opt": case "/z3opt": - if (ps.ConfirmArgumentCount(1)) - { - Z3Options.Add((!)args[ps.i]); + if (ps.ConfirmArgumentCount(1)) { + Z3Options.Add(cce.NonNull(args[ps.i])); } break; @@ -1158,61 +1292,64 @@ namespace Microsoft.Boogie case "-platform": case "/platform": - if (ps.ConfirmArgumentCount(1)) - { - StringCollection platformOptions = this.ParseNamedArgumentList(args[ps.i]); - if (platformOptions != null && platformOptions.Count > 0){ - try{ - this.TargetPlatform = (PlatformType)(!)Enum.Parse(typeof(PlatformType), (!)platformOptions[0]); - } - catch { - ps.Error("Bad /platform type '{0}'", platformOptions[0]); - break; - } - if (platformOptions.Count > 1){ - this.TargetPlatformLocation = platformOptions[1]; - if (!Directory.Exists(platformOptions[1])) { - ps.Error("/platform directory '{0}' does not exist", platformOptions[1]); - break; - } - } + if (ps.ConfirmArgumentCount(1)) { + StringCollection platformOptions = this.ParseNamedArgumentList(args[ps.i]); + if (platformOptions != null && platformOptions.Count > 0) { + try { + this.TargetPlatform = (PlatformType)cce.NonNull(Enum.Parse(typeof(PlatformType), cce.NonNull(platformOptions[0]))); + } catch { + ps.Error("Bad /platform type '{0}'", platformOptions[0]); + break; + } + if (platformOptions.Count > 1) { + this.TargetPlatformLocation = platformOptions[1]; + if (!Directory.Exists(platformOptions[1])) { + ps.Error("/platform directory '{0}' does not exist", platformOptions[1]); + break; + } } + } } break; case "-stdlib": case "/stdlib": - if (ps.ConfirmArgumentCount(1)) - { + if (ps.ConfirmArgumentCount(1)) { this.StandardLibraryLocation = args[ps.i]; } break; case "-Houdini": case "/Houdini": - this.houdiniEnabled=true; - if (ps.hasColonArgument) { - if (ps.ConfirmArgumentCount(1)) { - foreach (char c in (!)args[ps.i]) - { - switch (c) - { - case 'c': houdiniFlags.continueAtError = true; break; - case 'i': houdiniFlags.incremental = true; break; - default : ps.Error("Unknown houdini flag: " + c + "\n"); break; - } - } - } - } - break; - + this.houdiniEnabled = true; + if (ps.hasColonArgument) { + if (ps.ConfirmArgumentCount(1)) { + foreach (char c in cce.NonNull(args[ps.i])) { + switch (c) { + case 'c': + houdiniFlags.continueAtError = true; + break; + case 'i': + houdiniFlags.incremental = true; + break; + default: + ps.Error("Unknown houdini flag: " + c + "\n"); + break; + } + } + } + } + break; + default: - assume true; + Contract.Assume(true); bool option = false; if (ps.CheckBooleanFlag("printUnstructured", ref option)) { - expose(this) { + cce.BeginExpose(this); + { PrintUnstructured = option ? 1 : 0; } + cce.EndExpose(); } else if ( ps.CheckBooleanFlag("printDesugared", ref PrintDesugarings) || ps.CheckBooleanFlag("printInstrumented", ref PrintInstrumented) || @@ -1225,7 +1362,7 @@ namespace Microsoft.Boogie ps.CheckBooleanFlag("overlookTypeErrors", ref OverlookBoogieTypeErrors) || ps.CheckBooleanFlag("noVerify", ref Verify, false) || ps.CheckBooleanFlag("traceverify", ref TraceVerify) || - ps.CheckBooleanFlag("noConsistencyChecks", ref NoConsistencyChecks, true) || + ps.CheckBooleanFlag("noConsistencyChecks", ref noConsistencyChecks, true) || ps.CheckBooleanFlag("alwaysAssumeFreeLoopInvariants", ref AlwaysAssumeFreeLoopInvariants, true) || ps.CheckBooleanFlag("nologo", ref DontShowLogo) || ps.CheckBooleanFlag("noVerifyByDefault", ref NoVerifyByDefault) || @@ -1246,16 +1383,11 @@ namespace Microsoft.Boogie ps.CheckBooleanFlag("monomorphize", ref Monomorphize) || ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) || ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) - ) - { + ) { // one of the boolean flags matched - } - else if (ps.s.StartsWith("-") || ps.s.StartsWith("/")) - { + } else if (ps.s.StartsWith("-") || ps.s.StartsWith("/")) { ps.Error("unknown switch: {0}", ps.s); - } - else if (ps.ConfirmArgumentCount(0)) - { + } else if (ps.ConfirmArgumentCount(0)) { string filename = ps.s; string extension = Path.GetExtension(filename); if (extension != null) { @@ -1266,11 +1398,14 @@ namespace Microsoft.Boogie } break; } - expose(ps) ps.i = ps.nextIndex; + cce.BeginExpose(ps); + ps.i = ps.nextIndex; + cce.EndExpose(); } - - assume true; - if (ps.encounteredErrors) res *= 2; + + Contract.Assume(true); + if (ps.encounteredErrors) + res *= 2; if (res < 0) { // help requested Usage(); } else if (AttrHelpRequested) { @@ -1278,18 +1413,19 @@ namespace Microsoft.Boogie } else if (ps.encounteredErrors) { Console.WriteLine("Use /help for available options"); } - + SetProverOptions(); - - if (Trace) { BoogieDebug.DoPrinting = true; } // reuse the -trace option for debug printing + + if (Trace) { + BoogieDebug.DoPrinting = true; + } // reuse the -trace option for debug printing return res; } - private void SetProverOptions() - modifies this.*; - ensures TheProverFactory != null; - ensures vcVariety != VCVariety.Unspecified; - { + private void SetProverOptions() { + //modifies this.*; + Contract.Ensures(TheProverFactory != null); + Contract.Ensures(vcVariety != VCVariety.Unspecified); // expand macros in filenames, now that LogPrefix is fully determined ExpandFilename(ref XmlSinkFilename); ExpandFilename(ref PrintFile); @@ -1298,16 +1434,18 @@ namespace Microsoft.Boogie ExpandFilename(ref SMTLibOutputPath); ExpandFilename(ref PrintErrorModelFile); - assume XmlSink == null; // XmlSink is to be set here + Contract.Assume(XmlSink == null); // XmlSink is to be set here if (XmlSinkFilename != null) { XmlSink = new XmlSink(XmlSinkFilename); } - + if (TheProverFactory == null) { - expose(this) { + cce.BeginExpose(this); + { TheProverFactory = ProverFactory.Load("Z3"); ProverName = "Z3".ToUpper(); } + cce.EndExpose(); } if (vcVariety == VCVariety.Unspecified) { @@ -1322,33 +1460,36 @@ namespace Microsoft.Boogie LoopFrameConditions = 2; } } - + if (CEVPrint && PrintErrorModel == 0) { PrintErrorModel = 1; } - + switch (InductiveMinMax) { - case 1: case 2: case 4: case 5: + case 1: + case 2: + case 4: + case 5: ReflectAdd = true; // these InductiveMinMax modes imply ReflectAdd break; default: break; } - + if (MethodologySelection == Methodology.VisibleState) { OwnershipModelEncoding = OwnershipModelOption.Trivial; } - + if (UseArrayTheory) { Monomorphize = true; } - + if (LazyInlining > 0) { TypeEncodingMethod = TypeEncoding.Monomorphic; UseArrayTheory = true; UseAbstractInterpretation = false; } - + if (StratifiedInlining > 0) { TypeEncodingMethod = TypeEncoding.Monomorphic; UseArrayTheory = true; @@ -1358,34 +1499,41 @@ namespace Microsoft.Boogie - public bool UserWantsMethodLogging (string! methodFullName) - { - if (methodToLog == null) { return false; } - return methodToLog == "*" || methodFullName.IndexOf(methodToLog) >= 0; + public bool UserWantsMethodLogging(string methodFullName) { + Contract.Requires(methodFullName != null); + if (methodToLog == null) { + return false; + } + return methodToLog == "*" || methodFullName.IndexOf(methodToLog) >= 0; } - - public bool UserWantsToBreak (string! methodFullName) - { - if (methodToBreakOn == null) { return false; } - return methodFullName.IndexOf(methodToBreakOn) >= 0; + + public bool UserWantsToBreak(string methodFullName) { + Contract.Requires(methodFullName != null); + if (methodToBreakOn == null) { + return false; + } + return methodFullName.IndexOf(methodToBreakOn) >= 0; } - - public bool UserWantsToCheckRoutine(string! methodFullname) - { + + public bool UserWantsToCheckRoutine(string methodFullname) { + Contract.Requires(methodFullname != null); if (procsToCheck == null) { // no preference return true; } - return exists{string s in procsToCheck; 0 <= methodFullname.IndexOf(s)}; + return Contract.Exists(procsToCheck, s => 0 <= methodFullname.IndexOf(s)); } - public bool UserWantsToTranslateRoutine(Cci.Method! method, string! methodFullname) { + public bool UserWantsToTranslateRoutine(Cci.Method method, string methodFullname) { + Contract.Requires(methodFullname != null); + Contract.Requires(method != null); return UserWantsToTranslateRoutineInclude(method, methodFullname) && - !exists{string s in methodsToTranslateExclude; 0 <= methodFullname.IndexOf(s)}; + !Contract.Exists(methodsToTranslateExclude, s => 0 <= methodFullname.IndexOf(s)); } - - public bool UserWantsToTranslateRoutineInclude(Cci.Method! method, string! methodFullname) - { + + public bool UserWantsToTranslateRoutineInclude(Cci.Method method, string methodFullname) { + Contract.Requires(methodFullname != null); + Contract.Requires(method != null); if (methodsToTranslateSubstring == null && methodsToTranslateClass == null && methodsToTranslateClassQualified == null && @@ -1396,20 +1544,20 @@ namespace Microsoft.Boogie return true; } if (methodsToTranslateSubstring != null) { - if (exists{string s in methodsToTranslateSubstring; 0 <= methodFullname.IndexOf(s)}) { + if (Contract.Exists(methodsToTranslateSubstring, s => 0 <= methodFullname.IndexOf(s))) { return true; } } if (methodsToTranslateMethod != null) { string methodName = method.Name.Name; - assert methodsToTranslateMethod != null; + Contract.Assert(methodsToTranslateMethod != null); if (methodsToTranslateMethod.Contains(methodName)) { return true; } } if (methodsToTranslateMethodQualified != null && method.DeclaringType != null) { string methodName = method.DeclaringType.Name.Name + "." + method.Name.Name; - assert methodsToTranslateMethodQualified != null; + Contract.Assert(methodsToTranslateMethodQualified != null); if (methodsToTranslateMethodQualified.Contains(methodName)) { return true; } @@ -1450,7 +1598,8 @@ namespace Microsoft.Boogie /// /// Returns the file containing "method". Returns null f that information is not available. /// - static string GetSourceDocument(Cci.Method! method) { + static string GetSourceDocument(Cci.Method method) { + Contract.Requires(method != null); // Start by looking for a source context in the method itself. However, if the program // was read from a binary, then there is no source location for the method. If so, there // some other ways we might find a source location. @@ -1488,7 +1637,8 @@ namespace Microsoft.Boogie return null; // no source location found } - [Pure] static string GetSourceDocumentFromStatements(Cci.StatementList list) { + [Pure] + static string GetSourceDocumentFromStatements(Cci.StatementList list) { if (list != null) { foreach (Cci.Statement c in list) { if (c != null && c.SourceContext.Document != null) { @@ -1506,22 +1656,27 @@ namespace Microsoft.Boogie return null; } - class CommandLineParseState - { + class CommandLineParseState { public string s; public bool hasColonArgument; - public readonly string[]! args; + public readonly string[]/*!*/ args; public int i; public int nextIndex; public bool encounteredErrors; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(args != null); + Contract.Invariant(0 <= i && i <= args.Length); + Contract.Invariant(0 <= nextIndex && nextIndex <= args.Length); + + } + - invariant 0 <= i && i <= args.Length; - invariant 0 <= nextIndex && nextIndex <= args.Length; - public CommandLineParseState(string[]! args) - requires forall{int i in (0:args.Length); args[i] != null}; - ensures this.args == args; - { + public CommandLineParseState(string[] args) { + Contract.Requires(args != null); + Contract.Requires(Contract.ForAll(0, args.Length, i => args[i] != null)); + Contract.Ensures(this.args == args); this.s = null; // set later by client this.hasColonArgument = false; // set later by client this.args = args; @@ -1530,22 +1685,21 @@ namespace Microsoft.Boogie this.encounteredErrors = false; } - public bool CheckBooleanFlag(string! flagName, ref bool flag, bool valueWhenPresent) - modifies nextIndex, encounteredErrors, Console.Error.*; - { + public bool CheckBooleanFlag(string flagName, ref bool flag, bool valueWhenPresent) { + Contract.Requires(flagName != null); + //modifies nextIndex, encounteredErrors, Console.Error.*; bool flagPresent = false; - - if ((s == "/"+flagName || s == "-"+flagName) && ConfirmArgumentCount(0)) - { - flag = valueWhenPresent; - flagPresent = true; - } + + if ((s == "/" + flagName || s == "-" + flagName) && ConfirmArgumentCount(0)) { + flag = valueWhenPresent; + flagPresent = true; + } return flagPresent; } - - public bool CheckBooleanFlag(string! flagName, ref bool flag) - modifies nextIndex, encounteredErrors, Console.Error.*; - { + + public bool CheckBooleanFlag(string flagName, ref bool flag) { + Contract.Requires(flagName != null); + //modifies nextIndex, encounteredErrors, Console.Error.*; return CheckBooleanFlag(flagName, ref flag, true); } @@ -1553,14 +1707,12 @@ namespace Microsoft.Boogie /// If there is one argument and it is a non-negative integer, then set "arg" to that number and return "true". /// Otherwise, emit error message, leave "arg" unchanged, and return "false". /// - public bool GetNumericArgument(ref int arg) - modifies nextIndex, encounteredErrors, Console.Error.*; - { - if (this.ConfirmArgumentCount(1)) - { + public bool GetNumericArgument(ref int arg) { + //modifies nextIndex, encounteredErrors, Console.Error.*; + if (this.ConfirmArgumentCount(1)) { try { - assume args[i] != null; - assert args[i] is string; // needed to prove args[i].IsPeerConsistent + Contract.Assume(args[i] != null); + Contract.Assert(args[i] is string); // needed to prove args[i].IsPeerConsistent int d = Convert.ToInt32(this.args[this.i]); if (0 <= d) { arg = d; @@ -1575,16 +1727,15 @@ namespace Microsoft.Boogie Error("Invalid argument \"{0}\" to option {1}", args[this.i], this.s); return false; } - + /// /// If there is one argument and it is a non-negative integer less than "limit", /// then set "arg" to that number and return "true". /// Otherwise, emit error message, leave "arg" unchanged, and return "false". /// - public bool GetNumericArgument(ref int arg, int limit) - requires this.i < args.Length; - modifies nextIndex, encounteredErrors, Console.Error.*; - { + public bool GetNumericArgument(ref int arg, int limit) { + Contract.Requires(this.i < args.Length); + //modifies nextIndex, encounteredErrors, Console.Error.*; int a = arg; if (!GetNumericArgument(ref a)) { return false; @@ -1596,19 +1747,17 @@ namespace Microsoft.Boogie return false; } } - + /// /// If there is one argument and it is a non-negative real, then set "arg" to that number and return "true". /// Otherwise, emit an error message, leave "arg" unchanged, and return "false". /// - public bool GetNumericArgument(ref double arg) - modifies nextIndex, encounteredErrors, Console.Error.*; - { - if (this.ConfirmArgumentCount(1)) - { + public bool GetNumericArgument(ref double arg) { + //modifies nextIndex, encounteredErrors, Console.Error.*; + if (this.ConfirmArgumentCount(1)) { try { - assume args[i] != null; - assert args[i] is string; // needed to prove args[i].IsPeerConsistent + Contract.Assume(args[i] != null); + Contract.Assert(args[i] is string); // needed to prove args[i].IsPeerConsistent double d = Convert.ToDouble(this.args[this.i]); if (0 <= d) { arg = d; @@ -1623,71 +1772,68 @@ namespace Microsoft.Boogie Error("Invalid argument \"{0}\" to option {1}", args[this.i], this.s); return false; } - - public bool ConfirmArgumentCount(int argCount) - requires 0 <= argCount; - modifies nextIndex, encounteredErrors, Console.Error.*; - ensures result == ( !(hasColonArgument && argCount != 1) && !(args.Length < i + argCount) ); - { - if (hasColonArgument && argCount != 1) - { + + public bool ConfirmArgumentCount(int argCount) { + Contract.Requires(0 <= argCount); + //modifies nextIndex, encounteredErrors, Console.Error.*; + Contract.Ensures(Contract.Result() == (!(hasColonArgument && argCount != 1) && !(args.Length < i + argCount))); + if (hasColonArgument && argCount != 1) { Error("\"{0}\" cannot take a colon argument", s); nextIndex = args.Length; return false; - } - else if (args.Length < i + argCount) - { + } else if (args.Length < i + argCount) { Error("\"{0}\" expects {1} argument{2}", s, argCount.ToString(), (string)(argCount == 1 ? "" : "s")); nextIndex = args.Length; return false; - } - else - { + } else { nextIndex = i + argCount; return true; } } - public void Error(string! message, params string[]! args) - modifies encounteredErrors, Console.Error.*; - { + public void Error(string message, params string[] args) { + Contract.Requires(args != null); + Contract.Requires(message != null); + //modifies encounteredErrors, Console.Error.*; Console.Error.WriteLine("Boogie: Error: " + String.Format(message, args)); encounteredErrors = true; } } - public virtual StringCollection ParseNamedArgumentList(string argList){ - if (argList == null || argList.Length == 0) return null; + public virtual StringCollection ParseNamedArgumentList(string argList) { + if (argList == null || argList.Length == 0) + return null; StringCollection result = new StringCollection(); int i = 0; - for (int n = argList.Length; i < n;) - invariant 0 <= i; - { + for (int n = argList.Length; i < n; ) { + cce.LoopInvariant(0 <= i); int separatorIndex = this.GetArgumentSeparatorIndex(argList, i); - if (separatorIndex > i){ - result.Add(argList.Substring(i, separatorIndex-i)); - i = separatorIndex+1; + if (separatorIndex > i) { + result.Add(argList.Substring(i, separatorIndex - i)); + i = separatorIndex + 1; continue; } result.Add(argList.Substring(i)); break; - } + } return result; } - public int GetArgumentSeparatorIndex(string! argList, int startIndex) - requires 0 <= startIndex && startIndex <= argList.Length; - ensures result < argList.Length; - { + public int GetArgumentSeparatorIndex(string argList, int startIndex) { + Contract.Requires(argList != null); + Contract.Requires(0 <= startIndex && startIndex <= argList.Length); + Contract.Ensures(Contract.Result() < argList.Length); int commaIndex = argList.IndexOf(",", startIndex); int semicolonIndex = argList.IndexOf(";", startIndex); - if (commaIndex == -1) return semicolonIndex; - if (semicolonIndex == -1) return commaIndex; - if (commaIndex < semicolonIndex) return commaIndex; + if (commaIndex == -1) + return semicolonIndex; + if (semicolonIndex == -1) + return commaIndex; + if (commaIndex < semicolonIndex) + return commaIndex; return semicolonIndex; } - public static void AttributeUsage() - { + public static void AttributeUsage() { Console.WriteLine( @"Boogie: The following attributes are supported by this implementation. @@ -1772,15 +1918,16 @@ namespace Microsoft.Boogie private static bool printedHelp = false; - public static void Usage() - { - // Ensure that we only print the help message once, - // no matter how many enabling conditions for printing - // help were triggered. - if (printedHelp) { return; } - printedHelp = true; - - Console.WriteLine(@"Boogie: usage: Boogie [ option ... ] [ filename ... ] + public static void Usage() { + // Ensure that we only print the help message once, + // no matter how many enabling conditions for printing + // help were triggered. + if (printedHelp) { + return; + } + printedHelp = true; + + Console.WriteLine(@"Boogie: usage: Boogie [ option ... ] [ filename ... ] where