From b617dda87871573b826dada4af73fc48dce94f15 Mon Sep 17 00:00:00 2001 From: tabarbe Date: Fri, 20 Aug 2010 22:29:44 +0000 Subject: Boogie: Renaming core sources in preparation for port commit --- Source/Core/CommandLineOptions.cs | 2109 +++++++++++++++++++++++++++++++++++++ 1 file changed, 2109 insertions(+) create mode 100644 Source/Core/CommandLineOptions.cs (limited to 'Source/Core/CommandLineOptions.cs') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs new file mode 100644 index 00000000..6808be61 --- /dev/null +++ b/Source/Core/CommandLineOptions.cs @@ -0,0 +1,2109 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Collections; +using System.Collections.Generic; +using System.Collections.Specialized; +using System.IO; +using System.Diagnostics; +using Microsoft.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; } } + 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; + { + switch (value) { + 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"; + + public const long Megabyte = 1048576; + + // Flags and arguments + + 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) + { + if (pattern != null) { + pattern = pattern.Replace("@PREFIX@", LogPrefix).Replace("@TIME@", FileTimestamp); + string fn = Files.Count == 0 ? "" : Files[Files.Count-1]; + fn = fn.Replace('/', '-').Replace('\\', '-'); + pattern = pattern.Replace("@FILE@", fn); + } + } + + 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 bool PrintInstrumented = false; + public bool InstrumentWithAsserts = false; + public enum InstrumentationPlaces { LoopHeaders, Everywhere } + public InstrumentationPlaces InstrumentInfer = InstrumentationPlaces.LoopHeaders; + public bool PrintWithUniqueASTIds = false; + private string XmlSinkFilename = null; + [Peer] public XmlSink XmlSink = null; + public bool Wait = false; + public bool Trace = false; + public bool TraceTimes = false; + public bool NoResolve = false; + public bool NoTypecheck = false; + public bool OverlookBoogieTypeErrors = false; + public bool Verify = true; + public bool TraceVerify = false; + public int /*(0:3)*/ ErrorTrace = 1; + public bool IntraproceduralInfer = true; + public bool ContractInfer = false; + public bool UseUncheckedContracts = false; + public bool SimplifyLogFileAppend = false; + public bool SoundnessSmokeTest = false; + + private bool noConsistencyChecks = false; + public bool NoConsistencyChecks { + get {return !Verify ? true : noConsistencyChecks;} + set + modifies noConsistencyChecks; + {noConsistencyChecks = value;} + } + + public string DafnyPrintFile = null; + public bool Compile = true; + + public enum ProverWarnings { None, Stdout, Stderr } + public ProverWarnings PrintProverWarnings = ProverWarnings.None; + public int ProverShutdownLimit = 0; + + public enum SubsumptionOption { Never, NotForQuantifiers, Always } + public SubsumptionOption UseSubsumption = SubsumptionOption.Always; + + public bool AlwaysAssumeFreeLoopInvariants = false; + + public enum ShowEnvironment { Never, DuringPrint, Always } + public ShowEnvironment ShowEnv = ShowEnvironment.DuringPrint; + public bool DontShowLogo = false; + + public int CheckingLevel = 2; + invariant 0 <= CheckingLevel && CheckingLevel < 3; + 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 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 BvHandling Bitvectors = BvHandling.Z3Native; + + public bool UseArrayTheory = false; + 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 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 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 string ProverName; + [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 double VcsMaxCost = 1.0; + public double VcsPathJoinMult = 0.8; + public double VcsPathCostMult = 1.0; + public double VcsAssumeMult = 0.01; + public double VcsPathSplitMult = 0.5; // 0.5-always, 2-rarely do path splitting + public int VcsMaxSplits = 1; + public int VcsMaxKeepGoingSplits = 1; + public int VcsFinalAssertTimeout = 30; + public int VcsKeepGoingTimeout = 1; + public int VcsCores = 1; + public bool VcsDumpSplits = false; + + public bool houdiniEnabled = false; + public bool DebugRefuted = false; + + public XmlSink XmlRefuted + { + get { if (DebugRefuted) return XmlSink; else return null; } + } + + [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 + // + // Non-positive number indicates unbounded. + public long MaxProverMemory = 100 * Megabyte; + + // Minimum number of prover calls before restart + public int MinNumOfProverCalls = 5; + + 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 Inlining ProcedureInlining = Inlining.Assume; + public bool PrintInlined = false; + public bool ExtractLoops = false; + public int LazyInlining = 0; + public int StratifiedInlining = 0; + public int StratifiedInliningOption = 0; + public int RecursionBound = 500; + public string CoverageReporterPath = null; + + 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() + { + if (System.Type.GetType("Mono.Runtime") == null) { // MONO + TraceListenerCollection! dbl = Debug.Listeners; + assume dbl.IsPeerConsistent; // hangs off static field +#if WHIDBEY + dbl.Add(new ConsoleTraceListener()); +#else + dpl.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 + { + public bool Intervals = false; + public bool Constant = false; + public bool DynamicType = false; + public bool Nullness = false; + public bool Polyhedra = false; + public bool DebugStatistics = false; + + public bool AnySet + { + get + { + return Intervals + || Constant + || DynamicType + || Nullness + || Polyhedra; + } + } + } + public AiFlags! Ai = new AiFlags(); + + public class HoudiniFlags { + public bool continueAtError = false; + public bool incremental = false; + } + + public HoudiniFlags! houdiniFlags = new HoudiniFlags(); + + [Verify(false)] + public CommandLineOptions() { + // this is just to suppress verification. + } + + + /// + /// Parses the command-line arguments "args" into the global flag variables. The possible result + /// values are: + /// -2: an error occurred and help was requested + /// -1: no error occurred and help was requested + /// 1: no error occurred and help was not requested + /// 2: an error occurred and help was not requested + /// + /// 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; + { + // 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); + int res = 1; // the result value + + while (ps.i < args.Length) + invariant ps.IsPeerConsistent; + invariant ps.args == args; + { + ps.s = args[ps.i]; + assert ps.s != null; + ps.s = ps.s.Trim(); + + int colonIndex = ps.s.IndexOf(':'); + if (colonIndex >= 0 && (ps.s.StartsWith("-") || ps.s.StartsWith("/"))) + { + ps.hasColonArgument = true; + args[ps.i] = ps.s.Substring(colonIndex+1); + ps.s = ps.s.Substring(0, colonIndex); + } + else + { + expose(ps) { + ps.i++; + } + ps.hasColonArgument = false; + } + ps.nextIndex = ps.i; + + + switch (ps.s) + { + case "-help": + case "/help": + case "-?": + case "/?": + if (ps.ConfirmArgumentCount(0)) { + res = -1; // help requested + } + break; + + case "-attrHelp": + case "/attrHelp": + if (ps.ConfirmArgumentCount(0)) { + 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': + case '9': + StepsBeforeWidening = (int) char.GetNumericValue(c); break; + default: + ps.Error("Invalid argument '{0}' to option {1}", c.ToString(), ps.s); + break; + } + } + } + break; + + case "-noinfer": + case "/noinfer": + if (ps.ConfirmArgumentCount(0)) { + UseAbstractInterpretation = false; + } + break; + + case "-log": + case "/log": + if (ps.hasColonArgument) { + methodToLog = args[ps.i]; + ps.nextIndex = ps.i + 1; + } else { + 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(); + } + break; + + case "-launch": + case "/launch": + System.Diagnostics.Debugger.Launch(); + break; + + case "-proc": + case "/proc": + if (procsToCheck == null) { + procsToCheck = new List(); + } + if (ps.ConfirmArgumentCount(1)) { + procsToCheck.Add((!)args[ps.i]); + } + break; + + case "-translate": + case "/translate": + if (methodsToTranslateSubstring == null) { + methodsToTranslateSubstring = new List(); + } + if (ps.ConfirmArgumentCount(1)) { + methodsToTranslateSubstring.Add((!)args[ps.i]); + } + break; + + case "-trMethod": + case "/trMethod": + if (ps.ConfirmArgumentCount(1)) { + string m = (!)args[ps.i]; + if (0 <= m.IndexOf('.')) { + if (methodsToTranslateMethodQualified == null) { + methodsToTranslateMethodQualified = new List(); + } + methodsToTranslateMethodQualified.Add(m); + } else { + if (methodsToTranslateMethod == null) { + methodsToTranslateMethod = new List(); + } + methodsToTranslateMethod.Add(m); + } + } + break; + + case "-trClass": + case "/trClass": + if (ps.ConfirmArgumentCount(1)) { + string m = (!)args[ps.i]; + if (0 <= m.IndexOf('.')) { + if (methodsToTranslateClassQualified == null) { + methodsToTranslateClassQualified = new List(); + } + methodsToTranslateClassQualified.Add(m); + } else { + if (methodsToTranslateClass == null) { + methodsToTranslateClass = new List(); + } + methodsToTranslateClass.Add(m); + } + } + break; + + case "-trFile": + case "/trFile": + if (methodsToTranslateFile == null) { + methodsToTranslateFile = new List(); + } + if (ps.ConfirmArgumentCount(1)) { + methodsToTranslateFile.Add((!)args[ps.i]); + } + break; + + case "-trExclude": + case "/trExclude": + if (ps.ConfirmArgumentCount(1)) { + methodsToTranslateExclude.Add((!)args[ps.i]); + } + break; + + case "-xml": + case "/xml": + if (ps.ConfirmArgumentCount(1)) + { + XmlSinkFilename = args[ps.i]; + } + break; + + case "-print": + case "/print": + if (ps.ConfirmArgumentCount(1)) + { + PrintFile = args[ps.i]; + } + break; + + case "-dprint": + case "/dprint": + 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; + } + break; + } + + case "-contracts": + case "/contracts": + case "-c": + case "/c": + if (ps.ConfirmArgumentCount(1)) + { + ContractAssemblies.Add((!)args[ps.i]); + } + break; + + case "-proverLog": + case "/proverLog": + if (ps.ConfirmArgumentCount(1)) + { + SimplifyLogFilePath = args[ps.i]; + } + break; + + case "-logPrefix": + case "/logPrefix": + if (ps.ConfirmArgumentCount(1)) + { + string s = (!)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)) + { + 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]) + { + case "b": + case "Boogie": + case "boogie": + MethodologySelection = Methodology.Boogie; + break; + case "vs": + case "visible-state": + MethodologySelection = Methodology.VisibleState; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + 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 + } + } + 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 + } + } + 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": + { + int localChecks = 0; + ps.GetNumericArgument(ref localChecks, 2); + LocalModifiesChecks = (localChecks != 0); + } + break; + + case "-orderStrength": + case "/orderStrength": + ps.GetNumericArgument(ref OrderStrength, 2); + break; + + case "-summationStrength": + case "/summationStrength": + ps.GetNumericArgument(ref SummationAxiomStrength, 2); + break; + + case "-inductiveMinMax": + case "/inductiveMinMax": + ps.GetNumericArgument(ref InductiveMinMax, 6); + break; + + case "-fcoStrength": + case "/fcoStrength": + ps.GetNumericArgument(ref FCOStrength, 6); + break; + + case "-ownerModelEncoding": + case "/ownerModelEncoding": + if (ps.ConfirmArgumentCount(1)) + { + switch (args[ps.i]) + { + case "s": + case "standard": + OwnershipModelEncoding = OwnershipModelOption.Standard; + break; + case "e": + case "experimental": + OwnershipModelEncoding = OwnershipModelOption.Experimental; + break; + case "t": + case "trivial": + OwnershipModelEncoding = OwnershipModelOption.Trivial; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + break; + + case "-printModel": + case "/printModel": + if (ps.ConfirmArgumentCount(1)) + { + switch (args[ps.i]) + { + case "0": + PrintErrorModel = 0; + break; + case "1": + PrintErrorModel = 1; + break; + case "2": + PrintErrorModel = 2; + break; + case "4": + PrintErrorModel = 4; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + break; + + + case "-cev": + case "/cev": + if (ps.ConfirmArgumentCount(1)) + { + PrintErrorModelFile = args[ps.i]; + } + CEVPrint = true; + break; + + case "-printModelToFile": + case "/printModelToFile": + if (ps.ConfirmArgumentCount(1)) + { + PrintErrorModelFile = args[ps.i]; + } + break; + + + case "-enhancedErrorMessages": + case "/enhancedErrorMessages": + ps.GetNumericArgument(ref EnhancedErrorMessages, 2); + break; + + case "-forceBplErrors": + case "/forceBplErrors": + ForceBplErrors = true; + break; + + case "-bv": + case "/bv": + if (ps.ConfirmArgumentCount(1)) + { + if (TheProverFactory == null) { + TheProverFactory = ProverFactory.Load("Z3"); + ProverName = "Z3".ToUpper(); + } + + switch (args[ps.i]) + { + case "n": + Bitvectors = BvHandling.None; + break; + case "z": + Bitvectors = BvHandling.Z3Native; + break; + case "i": + Bitvectors = BvHandling.ToInt; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + 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 + } + } + break; + } + + case "-liveVariableAnalysis": + case "/liveVariableAnalysis": { + int lva = 0; + if (ps.GetNumericArgument(ref lva, 3)) { + LiveVariableAnalysis = lva; + } + break; + } + + case "-removeEmptyBlocks": + case "/removeEmptyBlocks": { + int reb = 0; + if (ps.GetNumericArgument(ref reb, 2)) { + RemoveEmptyBlocks = reb == 1; + } + break; + } + + case "-coalesceBlocks": + case "/coalesceBlocks": { + int cb = 0; + if (ps.GetNumericArgument(ref cb, 2)) { + CoalesceBlocks = cb == 1; + } + break; + } + + case "/DoomDebug": + vcVariety = VCVariety.Doomed; + useDoomDebug = true; + break; + + case "-vc": + case "/vc": + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) + { + case "s": + case "structured": + vcVariety = VCVariety.Structured; + break; + case "b": + case "block": + vcVariety = VCVariety.Block; + break; + case "l": + case "local": + vcVariety = VCVariety.Local; + break; + case "n": + case "nested": + vcVariety = VCVariety.BlockNested; + break; + case "m": + vcVariety = VCVariety.BlockNestedReach; + break; + case "r": + vcVariety = VCVariety.BlockReach; + break; + case "d": + case "dag": + vcVariety = VCVariety.Dag; + break; + case "doomed": + vcVariety = VCVariety.Doomed; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + break; + + case "-prover": + case "/prover": + if (ps.ConfirmArgumentCount(1)) { + TheProverFactory = ProverFactory.Load((!)args[ps.i]); + ProverName = ((!)args[ps.i]).ToUpper(); + } + break; + + case "-proverOpt": + case "/proverOpt": + if (ps.ConfirmArgumentCount(1)) { + ProverOptions.Add((!)args[ps.i]); + } + break; + + case "-extractLoops": + case "/extractLoops": + if (ps.ConfirmArgumentCount(0)) { + ExtractLoops = true; + } + break; + case "-inline": + case "/inline": + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) + { + case "none": + ProcedureInlining = Inlining.None; + break; + case "assert": + ProcedureInlining = Inlining.Assert; + break; + case "assume": + ProcedureInlining = Inlining.Assume; + break; + case "spec": + ProcedureInlining = Inlining.Spec; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + break; + case "-lazyInline": + case "/lazyInline": + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) + { + case "0": + LazyInlining = 0; + break; + case "1": + LazyInlining = 1; + break; + case "2": + LazyInlining = 2; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + break; + case "-stratifiedInline": + case "/stratifiedInline": + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) + { + case "0": + StratifiedInlining = 0; + break; + case "1": + StratifiedInlining = 1; + break; + default: + StratifiedInlining = Int32.Parse((!)args[ps.i]); + //ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + break; + case "-recursionBound": + case "/recursionBound": + if (ps.ConfirmArgumentCount(1)) { + RecursionBound = Int32.Parse((!)args[ps.i]); + } + break; + case "-coverageReporter": + case "/coverageReporter": + if (ps.ConfirmArgumentCount(1)) { + CoverageReporterPath = args[ps.i]; + } + break; + case "-stratifiedInlineOption": + case "/stratifiedInlineOption": + if (ps.ConfirmArgumentCount(1)) { + StratifiedInliningOption = Int32.Parse((!)args[ps.i]); + } + break; + case "-typeEncoding": + case "/typeEncoding": + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) + { + case "n": + case "none": + TypeEncodingMethod = TypeEncoding.None; + break; + case "p": + case "predicates": + TypeEncodingMethod = TypeEncoding.Predicates; + break; + case "a": + case "arguments": + TypeEncodingMethod = TypeEncoding.Arguments; + break; + case "m": + case "monomorphic": + TypeEncodingMethod = TypeEncoding.Monomorphic; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + break; + + case "-instrumentInfer": + case "/instrumentInfer": + if (ps.ConfirmArgumentCount(1)) { + switch (args[ps.i]) + { + case "e": + InstrumentInfer = InstrumentationPlaces.Everywhere; + break; + case "h": + InstrumentInfer = InstrumentationPlaces.LoopHeaders; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + break; + + case "-vcBrackets": + case "/vcBrackets": + ps.GetNumericArgument(ref BracketIdsInVC, 2); + break; + + case "-proverMemoryLimit": + case "/proverMemoryLimit": + { + int d = 0; + if (ps.GetNumericArgument(ref d)) { + MaxProverMemory = d * Megabyte; + } + break; + } + + case "-vcsMaxCost": + case "/vcsMaxCost": + ps.GetNumericArgument(ref VcsMaxCost); + break; + + case "-vcsPathJoinMult": + case "/vcsPathJoinMult": + ps.GetNumericArgument(ref VcsPathJoinMult); + break; + + case "-vcsPathCostMult": + case "/vcsPathCostMult": + ps.GetNumericArgument(ref VcsPathCostMult); + break; + + case "-vcsAssumeMult": + case "/vcsAssumeMult": + ps.GetNumericArgument(ref VcsAssumeMult); + break; + + case "-vcsPathSplitMult": + case "/vcsPathSplitMult": + ps.GetNumericArgument(ref VcsPathSplitMult); + break; + + case "-vcsMaxSplits": + case "/vcsMaxSplits": + ps.GetNumericArgument(ref VcsMaxSplits); + break; + + case "-vcsMaxKeepGoingSplits": + case "/vcsMaxKeepGoingSplits": + ps.GetNumericArgument(ref VcsMaxKeepGoingSplits); + break; + + case "-vcsFinalAssertTimeout": + case "/vcsFinalAssertTimeout": + ps.GetNumericArgument(ref VcsFinalAssertTimeout); + break; + + case "-vcsKeepGoingTimeout": + case "/vcsKeepGoingTimeout": + ps.GetNumericArgument(ref VcsKeepGoingTimeout); + break; + + case "-vcsCores": + case "/vcsCores": + ps.GetNumericArgument(ref VcsCores); + break; + + case "-simplifyMatchDepth": + case "/simplifyMatchDepth": + ps.GetNumericArgument(ref SimplifyProverMatchDepth); + break; + + case "-timeLimit": + case "/timeLimit": + ps.GetNumericArgument(ref ProverKillTime); + break; + + case "-smokeTimeout": + 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]); + } + break; + + case "-z3lets": + case "/z3lets": + ps.GetNumericArgument(ref Z3lets, 4); + break; + + 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; + } + } + } + } + break; + + case "-stdlib": + case "/stdlib": + 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; + + default: + assume true; + bool option = false; + if (ps.CheckBooleanFlag("printUnstructured", ref option)) { + expose(this) { + PrintUnstructured = option ? 1 : 0; + } + } else if ( + ps.CheckBooleanFlag("printDesugared", ref PrintDesugarings) || + ps.CheckBooleanFlag("printInstrumented", ref PrintInstrumented) || + ps.CheckBooleanFlag("printWithUniqueIds", ref PrintWithUniqueASTIds) || + ps.CheckBooleanFlag("wait", ref Wait) || + ps.CheckBooleanFlag("trace", ref Trace) || + ps.CheckBooleanFlag("traceTimes", ref TraceTimes) || + ps.CheckBooleanFlag("noResolve", ref NoResolve) || + ps.CheckBooleanFlag("noTypecheck", ref NoTypecheck) || + ps.CheckBooleanFlag("overlookTypeErrors", ref OverlookBoogieTypeErrors) || + ps.CheckBooleanFlag("noVerify", ref Verify, false) || + ps.CheckBooleanFlag("traceverify", ref TraceVerify) || + ps.CheckBooleanFlag("noConsistencyChecks", ref NoConsistencyChecks, true) || + ps.CheckBooleanFlag("alwaysAssumeFreeLoopInvariants", ref AlwaysAssumeFreeLoopInvariants, true) || + ps.CheckBooleanFlag("nologo", ref DontShowLogo) || + ps.CheckBooleanFlag("noVerifyByDefault", ref NoVerifyByDefault) || + ps.CheckBooleanFlag("useUncheckedContracts", ref UseUncheckedContracts) || + ps.CheckBooleanFlag("proverLogAppend", ref SimplifyLogFileAppend) || + ps.CheckBooleanFlag("checkInfer", ref InstrumentWithAsserts) || + ps.CheckBooleanFlag("interprocInfer", ref IntraproceduralInfer, false) || + ps.CheckBooleanFlag("restartProver", ref RestartProverPerVC) || + ps.CheckBooleanFlag("printInlined", ref PrintInlined) || + ps.CheckBooleanFlag("arithDistributionAxioms", ref UseArithDistributionAxioms) || + ps.CheckBooleanFlag("smoke", ref SoundnessSmokeTest) || + ps.CheckBooleanFlag("vcsDumpSplits", ref VcsDumpSplits) || + ps.CheckBooleanFlag("dbgRefuted", ref DebugRefuted) || + ps.CheckBooleanFlag("causalImplies", ref CausalImplies) || + ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd) || + ps.CheckBooleanFlag("z3types", ref Z3types) || + ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) || + 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("/")) + { + ps.Error("unknown switch: {0}", ps.s); + } + else if (ps.ConfirmArgumentCount(0)) + { + string filename = ps.s; + string extension = Path.GetExtension(filename); + if (extension != null) { + InputFileExtension = extension.ToLower(); + } + Files.Add(filename); + FileName = filename; + } + break; + } + expose(ps) ps.i = ps.nextIndex; + } + + assume true; + if (ps.encounteredErrors) res *= 2; + if (res < 0) { // help requested + Usage(); + } else if (AttrHelpRequested) { + AttributeUsage(); + } else if (ps.encounteredErrors) { + Console.WriteLine("Use /help for available options"); + } + + SetProverOptions(); + + 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; + { + // expand macros in filenames, now that LogPrefix is fully determined + ExpandFilename(ref XmlSinkFilename); + ExpandFilename(ref PrintFile); + ExpandFilename(ref DafnyPrintFile); + ExpandFilename(ref SimplifyLogFilePath); + ExpandFilename(ref SMTLibOutputPath); + ExpandFilename(ref PrintErrorModelFile); + + assume XmlSink == null; // XmlSink is to be set here + if (XmlSinkFilename != null) { + XmlSink = new XmlSink(XmlSinkFilename); + } + + if (TheProverFactory == null) { + expose(this) { + TheProverFactory = ProverFactory.Load("Z3"); + ProverName = "Z3".ToUpper(); + } + } + + if (vcVariety == VCVariety.Unspecified) { + vcVariety = TheProverFactory.DefaultVCVariety; + } + + if (LoopFrameConditions == -1) { + // /modifiesOnLoop not specified. Set its default depending on /localModifiesChecks + if (LocalModifiesChecks) { + LoopFrameConditions = 1; + } else { + LoopFrameConditions = 2; + } + } + + if (CEVPrint && PrintErrorModel == 0) { + PrintErrorModel = 1; + } + + switch (InductiveMinMax) { + 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; + UseAbstractInterpretation = false; + } + } + + + + public bool UserWantsMethodLogging (string! methodFullName) + { + 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 UserWantsToCheckRoutine(string! methodFullname) + { + if (procsToCheck == null) { + // no preference + return true; + } + return exists{string s in procsToCheck; 0 <= methodFullname.IndexOf(s)}; + } + + public bool UserWantsToTranslateRoutine(Cci.Method! method, string! methodFullname) { + return UserWantsToTranslateRoutineInclude(method, methodFullname) && + !exists{string s in methodsToTranslateExclude; 0 <= methodFullname.IndexOf(s)}; + } + + public bool UserWantsToTranslateRoutineInclude(Cci.Method! method, string! methodFullname) + { + if (methodsToTranslateSubstring == null && + methodsToTranslateClass == null && + methodsToTranslateClassQualified == null && + methodsToTranslateFile == null && + methodsToTranslateMethod == null && + methodsToTranslateMethodQualified == null) { + // no preference + return true; + } + if (methodsToTranslateSubstring != null) { + if (exists{string s in methodsToTranslateSubstring; 0 <= methodFullname.IndexOf(s)}) { + return true; + } + } + if (methodsToTranslateMethod != null) { + string methodName = method.Name.Name; + 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; + if (methodsToTranslateMethodQualified.Contains(methodName)) { + return true; + } + } + if (method.DeclaringType != null) { + if (methodsToTranslateClass != null) { + string className = method.DeclaringType.Name.Name; + if (methodsToTranslateClass.Contains(className)) { + return true; + } + } + if (methodsToTranslateClassQualified != null) { + string className = method.DeclaringType.FullName; + if (className != null) { + className = className.Replace('+', '.'); + if (methodsToTranslateClassQualified.Contains(className)) { + return true; + } + } + } + } + if (methodsToTranslateFile != null) { + string methodFilename = GetSourceDocument(method); + if (methodFilename != null) { + string path = methodFilename; + if (path != null) { + string filename = Path.GetFileName(path); + if (methodsToTranslateFile.Contains(filename)) { + return true; + } + } + } + } + // the method is not among the desired routines + return false; + } + + /// + /// Returns the file containing "method". Returns null f that information is not available. + /// + static string GetSourceDocument(Cci.Method! method) { + // 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. + if (method.SourceContext.Document != null) { + return method.SourceContext.Document.Name; + } + // Try to find a source location in the method's contract + if (method.Contract != null) { + if (method.Contract.Requires != null) { + foreach (Cci.Requires c in method.Contract.Requires) { + if (c != null && c.SourceContext.Document != null) { + return c.SourceContext.Document.Name; + } + } + } + if (method.Contract.Modifies != null) { + foreach (Cci.Expression c in method.Contract.Modifies) { + if (c != null && c.SourceContext.Document != null) { + return c.SourceContext.Document.Name; + } + } + } + if (method.Contract.Ensures != null) { + foreach (Cci.Ensures c in method.Contract.Ensures) { + if (c != null && c.SourceContext.Document != null) { + return c.SourceContext.Document.Name; + } + } + } + } + // As a last attempt, look for a source location among the statements + if (method.Body != null) { + return GetSourceDocumentFromStatements(method.Body.Statements); + } + return null; // no source location found + } + + [Pure] static string GetSourceDocumentFromStatements(Cci.StatementList list) { + if (list != null) { + foreach (Cci.Statement c in list) { + if (c != null && c.SourceContext.Document != null) { + return c.SourceContext.Document.Name; + } + if (c is Cci.Block) { + Cci.Block b = (Cci.Block)c; + string n = GetSourceDocumentFromStatements(b.Statements); + if (n != null) { + return n; + } + } + } + } + return null; + } + + class CommandLineParseState + { + public string s; + public bool hasColonArgument; + public readonly string[]! args; + public int i; + public int nextIndex; + public bool encounteredErrors; + + 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; + { + this.s = null; // set later by client + this.hasColonArgument = false; // set later by client + this.args = args; + this.i = 0; + this.nextIndex = 0; // set later by client + this.encounteredErrors = false; + } + + public bool CheckBooleanFlag(string! flagName, ref bool flag, bool valueWhenPresent) + modifies nextIndex, encounteredErrors, Console.Error.*; + { + bool flagPresent = false; + + 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.*; + { + return CheckBooleanFlag(flagName, ref flag, true); + } + + /// + /// 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)) + { + try { + assume args[i] != null; + assert args[i] is string; // needed to prove args[i].IsPeerConsistent + int d = Convert.ToInt32(this.args[this.i]); + if (0 <= d) { + arg = d; + return true; + } + } catch (System.FormatException) { + } catch (System.OverflowException) { + } + } else { + return false; + } + 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.*; + { + int a = arg; + if (!GetNumericArgument(ref a)) { + return false; + } else if (a < limit) { + arg = a; + return true; + } else { + 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 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)) + { + try { + assume args[i] != null; + assert args[i] is string; // needed to prove args[i].IsPeerConsistent + double d = Convert.ToDouble(this.args[this.i]); + if (0 <= d) { + arg = d; + return true; + } + } catch (System.FormatException) { + } catch (System.OverflowException) { + } + } else { + return false; + } + 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) + { + Error("\"{0}\" cannot take a colon argument", s); + nextIndex = args.Length; + return false; + } + 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 + { + nextIndex = i + argCount; + return true; + } + } + + public void Error(string! message, params string[]! args) + 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; + StringCollection result = new StringCollection(); + int i = 0; + for (int n = argList.Length; i < n;) + invariant 0 <= i; + { + int separatorIndex = this.GetArgumentSeparatorIndex(argList, i); + 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; + { + 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; + return semicolonIndex; + } + + public static void AttributeUsage() + { + Console.WriteLine( +@"Boogie: The following attributes are supported by this implementation. + + ---- On axioms ------------------------------------------------------------- + + {:inline true} + Works on axiom of the form: + (forall VARS :: f(VARS) = expr(VARS)) + Makes Boogie replace f(VARS) with expr(VARS) everywhere just before + doing VC generation. + + {:ignore ""p,q..""} + Exclude the axiom when generating VC for a prover supporting any + of the features 'p', 'q', ... + All the provers support the feature 'all'. + Simplify supports 'simplify' and 'simplifyLike'. + Z3 supports 'z3', 'simplifyLike' and either 'bvInt' (if the /bv:i + option is passed) or 'bvDefSem' (for /bv:z). + + ---- On implementations and procedures ------------------------------------- + + {:inline N} + Inline given procedure (can be also used on implementation). + N should be a non-negative number and represents the inlining depth. + With /inline:assume call is replaced with ""assume false"" once inlining depth is reached. + With /inline:assert call is replaced with ""assert false"" once inlining depth is reached. + With /inline:spec call is left as is once inlining depth is reached. + With the above three options, methods with the attribute {:inline N} are not verified. + With /inline:none the entire attribute is ignored. + + {:verify false} + Skip verification of an implementation. + + {:forceBvZ3Native true} + Verify the given implementation with the native Z3 bitvector + handling. Only works if /bv:i (or /bv:z, but then it does not do + anything) is given on the command line. + + {:forceBvInt true} + Use int translation for the given implementation. Only work with + /bv:z (or /bv:i). + + {:vcs_max_cost N} + {:vcs_max_splits N} + {:vcs_max_keep_going_splits N} + Per-implementation versions of + /vcsMaxCost, /vcsMaxSplits and /vcsMaxKeepGoingSplits. + + ---- On functions ---------------------------------------------------------- + + {:bvbuiltin ""spec""} + Z3 specific, used only with /bv:z. + + {:bvint ""fn""} + With /bv:i rewrite the function to function symbol 'fn', except if + the 'fn' is 'id', in which case just strip the function altogether. + + {:never_pattern true} + Terms starting with this function symbol will never be + automatically selected as patterns. It does not prevent them + from being used inside the triggers, and does not affect explicit + trigger annotations. Internally it works by adding {:nopats ...} + annotations to quantifiers. + + ---- On variables ---------------------------------------------------------- + + {:existential true} + Marks a global Boolean variable as existentially quantified. If + used in combination with option /contractInfer Boogie will check + whether there exists a Boolean assignment to the existentials + that makes all verification conditions valid. Without option + /contractInfer the attribute is ignored. + + ---- On assert statements -------------------------------------------------- + + {:subsumption n} + Overrides the /subsumption command-line setting for this assertion. + + ---- The end --------------------------------------------------------------- +"); + } + + 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 ... ] + where