summaryrefslogtreecommitdiff
path: root/Source/Core/CommandLineOptions.cs
diff options
context:
space:
mode:
authorGravatar tabarbe <unknown>2010-08-20 22:32:24 +0000
committerGravatar tabarbe <unknown>2010-08-20 22:32:24 +0000
commit72b39a6962d7f6c7ca1aab9919791238c7baba3f (patch)
tree75bb9c1b956d1b368f4cf2983a20a913211dd350 /Source/Core/CommandLineOptions.cs
parent96d9624e9e22dbe9090e0bd7d538cafbf0a16463 (diff)
Boogie: Committing changed source files
Diffstat (limited to 'Source/Core/CommandLineOptions.cs')
-rw-r--r--Source/Core/CommandLineOptions.cs1276
1 files changed, 712 insertions, 564 deletions
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<string>() != 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<string>() != 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<string>() != null);
+ return _toolname;
+ }
+ }
+ public string/*!*/ Version {
+ get {
+ Contract.Ensures(Contract.Result<string>() != 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<string!>! Files = new List<string!>();
- public List<string!>! ContractAssemblies = new List<string!>();
-
- public string! FileTimestamp = ((!)DateTime.Now.ToString("o")).Replace(':', '.');
- public void ExpandFilename(ref string pattern)
- {
+
+ [Peer]
+ public List<string/*!*/>/*!*/ Files = new List<string/*!*/>();
+ public List<string/*!*/>/*!*/ ContractAssemblies = new List<string/*!*/>();
+
+ 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<string!>! ProverOptions = new List<string!>();
+ [Peer]
+ public List<string/*!*/>/*!*/ ProverOptions = new List<string/*!*/>();
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<string!>! Z3Options = new List<string!>();
+ [ContractInvariantMethod]
+ void ObjectInvariant4() {
+ Contract.Invariant(cce.NonNullElements(Z3Options));
+ Contract.Invariant(0 <= Z3lets && Z3lets < 4);
+ }
+
+ [Peer]
+ public List<string/*!*/>/*!*/ Z3Options = new List<string/*!*/>();
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<string!> procsToCheck = null; // null means "no restriction"
- [Rep] private List<string!> methodsToTranslateSubstring = null; // null means "no restriction"
- [Rep] private List<string!> methodsToTranslateMethod = null; // null means "no restriction"
- [Rep] private List<string!> methodsToTranslateMethodQualified = null; // null means "no restriction"
- [Rep] private List<string!> methodsToTranslateClass = null; // null means "no restriction"
- [Rep] private List<string!> methodsToTranslateClassQualified = null; // null means "no restriction"
- [Rep] private List<string!> methodsToTranslateFile = null; // null means "no restriction"
- [Rep] private List<string!>! methodsToTranslateExclude = new List<string!>();
-
- 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<string/*!*/> procsToCheck = null; // null means "no restriction"
+ [Rep]
+ private List<string/*!*/> methodsToTranslateSubstring = null; // null means "no restriction"
+ [Rep]
+ private List<string/*!*/> methodsToTranslateMethod = null; // null means "no restriction"
+ [Rep]
+ private List<string/*!*/> methodsToTranslateMethodQualified = null; // null means "no restriction"
+ [Rep]
+ private List<string/*!*/> methodsToTranslateClass = null; // null means "no restriction"
+ [Rep]
+ private List<string/*!*/> methodsToTranslateClassQualified = null; // null means "no restriction"
+ [Rep]
+ private List<string/*!*/> methodsToTranslateFile = null; // null means "no restriction"
+ [Rep]
+ private List<string/*!*/>/*!*/ methodsToTranslateExclude = new List<string/*!*/>();
+
+ 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
/// </summary>
/// <param name="args">Consumed ("captured" and possibly modified) by the method.</param>
[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<int>() && Contract.Result<int>() <= 2 && Contract.Result<int>() != 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<string!>();
+ procsToCheck = new List<string/*!*/>();
}
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<string!>();
+ methodsToTranslateSubstring = new List<string/*!*/>();
}
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<string!>();
+ methodsToTranslateMethodQualified = new List<string/*!*/>();
}
methodsToTranslateMethodQualified.Add(m);
} else {
if (methodsToTranslateMethod == null) {
- methodsToTranslateMethod = new List<string!>();
+ methodsToTranslateMethod = new List<string/*!*/>();
}
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<string!>();
+ methodsToTranslateClassQualified = new List<string/*!*/>();
}
methodsToTranslateClassQualified.Add(m);
} else {
if (methodsToTranslateClass == null) {
- methodsToTranslateClass = new List<string!>();
+ methodsToTranslateClass = new List<string/*!*/>();
}
methodsToTranslateClass.Add(m);
}
@@ -500,109 +654,100 @@ namespace Microsoft.Boogie
case "-trFile":
case "/trFile":
if (methodsToTranslateFile == null) {
- methodsToTranslateFile = new List<string!>();
+ methodsToTranslateFile = new List<string/*!*/>();
}
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
/// <summary>
/// Returns the file containing "method". Returns null f that information is not available.
/// </summary>
- 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".
/// </summary>
- 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;
}
-
+
/// <summary>
/// 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".
/// </summary>
- 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;
}
}
-
+
/// <summary>
/// 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".
/// </summary>
- 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<bool>() == (!(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<int>() < 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 <option> is one of
---- General options -------------------------------------------------------
@@ -1907,11 +2054,12 @@ namespace Microsoft.Boogie
---- Inference options -----------------------------------------------------
/infer:<flags> : use abstract interpretation to infer invariants
- The default is /infer:i" // This is not 100% true, as the /infer ALWAYS creates
- // a multilattice, whereas if nothing is specified then
- // intervals are isntantiated WITHOUT being embedded in
- // a multilattice
- + @"
+ The default is /infer:i"
+ // This is not 100% true, as the /infer ALWAYS creates
+ // a multilattice, whereas if nothing is specified then
+ // intervals are isntantiated WITHOUT being embedded in
+ // a multilattice
+ + @"
<flags> are as follows (missing <flags> means all)
i = intervals
c = constant propagation
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-18 19:56:54 +0000