diff options
Diffstat (limited to 'Source/Core/CommandLineOptions.cs')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 64 |
1 files changed, 16 insertions, 48 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 73fa8946..4192259d 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -575,8 +575,6 @@ namespace Microsoft.Boogie { public string CoverageReporterPath = null;
public Process coverageReporter = null; // used internally for debugging
- public bool DoPredication = false;
-
public enum TypeEncoding {
None,
Predicates,
@@ -609,26 +607,9 @@ namespace Microsoft.Boogie { }
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 J_Trivial = false;
public bool J_Intervals = false;
public bool DebugStatistics = false;
-
- public bool AnySet {
- get {
- return Intervals
- || Constant
- || DynamicType
- || Nullness
- || Polyhedra
- || J_Trivial
- || J_Intervals;
- }
- }
}
public AiFlags/*!*/ Ai = new AiFlags();
@@ -639,26 +620,6 @@ namespace Microsoft.Boogie { 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 't':
Ai.J_Trivial = true;
UseAbstractInterpretation = true;
@@ -697,12 +658,6 @@ namespace Microsoft.Boogie { }
return true;
- case "logInfer":
- if (ps.ConfirmArgumentCount(0)) {
- Microsoft.AbstractInterpretationFramework.Lattice.LogSwitch = true;
- }
- return true;
-
case "break":
case "launch":
if (ps.ConfirmArgumentCount(0)) {
@@ -1133,6 +1088,18 @@ namespace Microsoft.Boogie { ps.GetNumericArgument(ref VcsCores);
return true;
+ case "vcsLoad":
+ double load = 0.0;
+ if (ps.GetNumericArgument(ref load)) {
+ if (3.0 <= load) {
+ ps.Error("surprisingly high load specified; got {0}, expected nothing above 3.0", load.ToString());
+ load = 3.0;
+ }
+ int p = (int)Math.Round(System.Environment.ProcessorCount * load);
+ VcsCores = p < 1 ? 1 : p;
+ }
+ return true;
+
case "simplifyMatchDepth":
ps.GetNumericArgument(ref SimplifyProverMatchDepth);
return true;
@@ -1234,8 +1201,7 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||
ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||
ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
- ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
- ps.CheckBooleanFlag("predicate", ref DoPredication)
+ ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops)
) {
// one of the boolean flags matched
return true;
@@ -1502,7 +1468,6 @@ namespace Microsoft.Boogie { perform interprocedural inference (deprecated, not supported)
/contractInfer
perform procedure contract inference
- /logInfer print debug output during inference
/instrumentInfer
h - instrument inferred invariants only at beginning of
loop headers (default)
@@ -1642,6 +1607,9 @@ namespace Microsoft.Boogie { Warning: Affects error reporting.
/vcsCores:<n>
Try to verify <n> VCs at once. Defaults to 1.
+ /vcsLoad:<f> Sets vcsCores to the machine's ProcessorCount * f,
+ rounded to the nearest integer (where 0.0 <= f <= 3.0),
+ but never to less than 1.
---- Prover options --------------------------------------------------------
|