diff options
| author |  akashlal <unknown> | 2010-08-23 19:23:48 +0000 |
|---|---|---|
| committer | akashlal <unknown> | 2010-08-23 19:23:48 +0000 |
| commit | 913dce83219e9a9e6de2d148e5edea8adca77ed6 (patch) | |
| tree | b4283d2f935de3bd4b05d3389f3482567be496fc /Source | |
| parent | 238465abbbc96e0548f35f2746f40c93ced0c513 (diff) | |
Added a short description of new flags added to Boogie.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 20a2fede..f9f7dfab 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -2130,6 +2130,10 @@ namespace Microsoft.Boogie { spec
/printInlined : print the implementation after inlining calls to
procedures with the :inline attribute (works with /inline)
+ /lazyInline:1 : Use the lazy inlining algorithm
+ /stratifiedInline:1 : Use the stratified inlining algorithm
+ /recursionBound:<n> : Set the recursion bound for stratified inlining to
+ be n (default 500)
/smoke : Soundness Smoke Test: try to stick assert false; in some
places in the BPL and see if we can still prove it
/smokeTimeout:<n> : Timeout, in seconds, for a single theorem prover
|