diff options
| author |  akashlal <unknown> | 2010-08-20 13:41:21 +0000 |
|---|---|---|
| committer | akashlal <unknown> | 2010-08-20 13:41:21 +0000 |
| commit | 33db8d179f2531a63456f02ade0062e0c48094f4 (patch) | |
| tree | 56832695d10a1c22966ce81ff3395845054f662f | |
| parent | d06b5bf7faae69a0348a1c599c176f184baaa828 (diff) | |
Added user option for bounding inlining depth
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 7 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 2 |
2 files changed, 8 insertions, 1 deletions
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index d60e7323..6808be61 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -228,6 +228,7 @@ namespace Microsoft.Boogie 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 };
@@ -993,6 +994,12 @@ namespace Microsoft.Boogie }
}
break; + case "-recursionBound":
+ case "/recursionBound":
+ if (ps.ConfirmArgumentCount(1)) {
+ RecursionBound = Int32.Parse((!)args[ps.i]);
+ }
+ break; case "-coverageReporter":
case "/coverageReporter":
if (ps.ConfirmArgumentCount(1)) {
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index b77117ff..42626ed7 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2010,7 +2010,7 @@ namespace VC { int bound = 1;
bool done = false;
- while (bound < 500 && !done)
+ while (bound < CommandLineOptions.Clo.RecursionBound && !done)
{
while (true)
{
|