diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-10 16:12:06 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-10 16:12:06 -0700 |
| commit | 68d57324e25c44f022e55bbc55fffd4e22842928 (patch) | |
| tree | 9b80798f1db3d210257dfbed0dae07280d320256 /Source/BoogieDriver/BoogieDriver.cs | |
| parent | dad509d9e6c28b6b03e93afe10346dcc63433b57 (diff) | |
Boogie: added /tracePOs option for printing out number of proof obligations without also printing out the verification times
Diffstat (limited to 'Source/BoogieDriver/BoogieDriver.cs')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 66582173..1653b723 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -237,10 +237,9 @@ namespace Microsoft.Boogie { /// Print newline after the message.
/// </summary>
public static void Inform(string s) {
- if (!CommandLineOptions.Clo.Trace) {
- return;
+ if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations) {
+ Console.WriteLine(s);
}
- Console.WriteLine(s);
}
static void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories) {
@@ -688,9 +687,9 @@ namespace Microsoft.Boogie { List<Counterexample/*!*/>/*?*/ errors;
DateTime start = new DateTime(); // to please compiler's definite assignment rules
- if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {
+ if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations || CommandLineOptions.Clo.XmlSink != null) {
start = DateTime.UtcNow;
- if (CommandLineOptions.Clo.Trace) {
+ if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations) {
Console.WriteLine();
Console.WriteLine("Verifying {0} ...", impl.Name);
}
@@ -741,11 +740,12 @@ namespace Microsoft.Boogie { string timeIndication = "";
DateTime end = DateTime.UtcNow;
TimeSpan elapsed = end - start;
- if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {
- if (CommandLineOptions.Clo.Trace) {
- int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;
- timeIndication = string.Format(" [{0:F3} s, {1} proof obligation{2}] ", elapsed.TotalSeconds, poCount, poCount == 1 ? "" : "s");
- }
+ if (CommandLineOptions.Clo.Trace) {
+ int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;
+ timeIndication = string.Format(" [{0:F3} s, {1} proof obligation{2}] ", elapsed.TotalSeconds, poCount, poCount == 1 ? "" : "s");
+ } else if (CommandLineOptions.Clo.TraceProofObligations) {
+ int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;
+ timeIndication = string.Format(" [{0} proof obligation{1}] ", poCount, poCount == 1 ? "" : "s");
}
ProcessOutcome(outcome, errors, timeIndication, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);
|