diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-11-15 18:48:02 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-11-15 18:48:02 -0800 |
| commit | 73b9d30f3b18425e52ef80453977d8608a1db09b (patch) | |
| tree | b2b98d7ba6846bee0a6c8f4a22e67eb620d493d8 /Source/BoogieDriver | |
| parent | 78160fbd9492cf88e620a859a405fe9a49a09c54 (diff) | |
Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLineOptions to separate the options that belong to these 3 tools.
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 83e6009d..028ff1dd 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -35,8 +35,10 @@ namespace Microsoft.Boogie { public static void Main(string[] args) {
Contract.Requires(cce.NonNullElements(args));
+ CommandLineOptions.Install(new CommandLineOptions());
+
CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;
- if (CommandLineOptions.Clo.Parse(args) != 1) {
+ if (!CommandLineOptions.Clo.Parse(args)) {
goto END;
}
if (CommandLineOptions.Clo.Files.Count == 0) {
@@ -77,7 +79,6 @@ namespace Microsoft.Boogie { goto END;
}
}
- CommandLineOptions.Clo.RunningBoogieOnSsc = false;
ProcessFiles(CommandLineOptions.Clo.Files);
END:
@@ -223,9 +224,9 @@ namespace Microsoft.Boogie { Contract.Requires(0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories);
Console.WriteLine();
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
- Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");
+ Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");
} else {
- Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");
+ Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");
}
if (inconclusives != 0) {
Console.Write(", {0} inconclusive{1}", inconclusives, inconclusives == 1 ? "" : "s");
|