diff options
| author |  MichalMoskal <unknown> | 2010-10-12 01:18:45 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2010-10-12 01:18:45 +0000 |
| commit | 45fb2f73118bf4010ad08757122d829c76e676d3 (patch) | |
| tree | e67f8006ad0e4a72f6fb2340ae14e6716452fe4d /Source/Core | |
| parent | 2b1ddfbe8bcd48da4cab27e06078de59eecc8f40 (diff) | |
Make the -mv option use the new Model class.
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 4196670f..b63b82cc 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -192,7 +192,6 @@ namespace Microsoft.Boogie { Contract.Invariant(-1 <= LoopFrameConditions && LoopFrameConditions < 3);
Contract.Invariant(0 <= ModifiesDefault && ModifiesDefault < 7);
Contract.Invariant((0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4);
- Contract.Invariant(0 <= ModelView && ModelView < 2);
Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2);
Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9);
Contract.Invariant(-1 <= BracketIdsInVC && BracketIdsInVC <= 1);
@@ -230,7 +229,7 @@ namespace Microsoft.Boogie { public int PrintErrorModel = 0;
public string PrintErrorModelFile = null;
public bool CEVPrint = false;
- public int ModelView = 1;
+ public string/*?*/ ModelViewFile = null;
public int EnhancedErrorMessages = 0;
public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present
public enum BvHandling {
@@ -922,7 +921,9 @@ namespace Microsoft.Boogie { case "-mv":
case "/mv":
- ps.GetNumericArgument(ref ModelView, 2);
+ if (ps.ConfirmArgumentCount(1)) {
+ ModelViewFile = args[ps.i];
+ }
break;
case "-printModelToFile":
|