diff options
author | stobies <unknown> | 2009-09-07 09:50:49 +0000 |
---|---|---|
committer | stobies <unknown> | 2009-09-07 09:50:49 +0000 |
commit | deb203b5944c966d72c2884a425a450e93d49ad3 (patch) | |
tree | 45e2e7ae67ba7ca179030ac8e8646cd330264d0b | |
parent | a4f2bf6414f35907ab135cc6723683fe632467c4 (diff) |
Use callback mechanism to report prover warnings; do not just write them to stdout/stderr
-rw-r--r-- | Source/Provers/Simplify/Prover.ssc | 27 | ||||
-rw-r--r-- | Source/Provers/Z3/Prover.ssc | 2 | ||||
-rw-r--r-- | Source/VCGeneration/Check.ssc | 18 | ||||
-rw-r--r-- | Source/VCGeneration/ConditionGeneration.ssc | 4 | ||||
-rw-r--r-- | Source/VCGeneration/VC.ssc | 5 |
5 files changed, 34 insertions, 22 deletions
diff --git a/Source/Provers/Simplify/Prover.ssc b/Source/Provers/Simplify/Prover.ssc index f89d6a42..641c81f4 100644 --- a/Source/Provers/Simplify/Prover.ssc +++ b/Source/Provers/Simplify/Prover.ssc @@ -110,23 +110,6 @@ namespace Microsoft.Boogie.Simplify catch (System.ComponentModel.Win32Exception) { /* already exiting */ }
}
- public static void ReportWarning(string! w)
- modifies Console.Out.*, Console.Error.*;
- {
- switch (CommandLineOptions.Clo.PrintProverWarnings) {
- case CommandLineOptions.ProverWarnings.None:
- break;
- case CommandLineOptions.ProverWarnings.Stdout:
- Console.WriteLine("Prover warning: " + w);
- break;
- case CommandLineOptions.ProverWarnings.Stderr:
- Console.Error.WriteLine("Prover warning: " + w);
- break;
- default:
- assume false; // unexpected case
- }
- }
-
public virtual void AddAxioms(string! s)
modifies this.*;
modifies Console.Out.*, Console.Error.*;
@@ -440,7 +423,7 @@ namespace Microsoft.Boogie.Simplify } while (Char.IsWhiteSpace((char)ch));
while (ch == 'W') {
- ch = ConsumeWarnings(ch);
+ ch = ConsumeWarnings(ch, null);
}
Expect(ch, ">\t");
@@ -496,7 +479,7 @@ namespace Microsoft.Boogie.Simplify int ch = FromReadChar();
while (ch == 'W')
{
- ch = ConsumeWarnings(ch);
+ ch = ConsumeWarnings(ch, handler);
}
if (ch == 'E')
{
@@ -574,7 +557,7 @@ namespace Microsoft.Boogie.Simplify return theLabels;
}
- int ConsumeWarnings(int ch)
+ int ConsumeWarnings(int ch, Microsoft.Boogie.ProverInterface.ErrorHandler handler)
requires ch == 'W';
modifies this.*;
modifies Console.Out.*, Console.Error.*;
@@ -590,7 +573,9 @@ namespace Microsoft.Boogie.Simplify FromReadLine(); // blank line
FromReadLine(); // expression (entire quantifier)
}
- ReportWarning(w);
+
+ if (handler != null) handler.OnProverWarning(w);
+
ch = FromReadChar();
if (ch == '\n')
{
diff --git a/Source/Provers/Z3/Prover.ssc b/Source/Provers/Z3/Prover.ssc index d3212a9c..13c71814 100644 --- a/Source/Provers/Z3/Prover.ssc +++ b/Source/Provers/Z3/Prover.ssc @@ -247,7 +247,7 @@ namespace Microsoft.Boogie.Z3 if (line.StartsWith("WARNING: ")) {
string w = line.Substring(9);
- ReportWarning(w);
+ handler.OnProverWarning(w);
continue;
}
diff --git a/Source/VCGeneration/Check.ssc b/Source/VCGeneration/Check.ssc index f0d6c558..ca434ec5 100644 --- a/Source/VCGeneration/Check.ssc +++ b/Source/VCGeneration/Check.ssc @@ -326,6 +326,24 @@ namespace Microsoft.Boogie {
}
+ public virtual void OnProverWarning(string! message)
+ modifies Console.Out.*, Console.Error.*;
+ {
+ switch (CommandLineOptions.Clo.PrintProverWarnings) {
+ case CommandLineOptions.ProverWarnings.None:
+ break;
+ case CommandLineOptions.ProverWarnings.Stdout:
+ Console.WriteLine("Prover warning: " + message);
+ break;
+ case CommandLineOptions.ProverWarnings.Stderr:
+ Console.Error.WriteLine("Prover warning: " + message);
+ break;
+ default:
+ assume false; // unexpected case
+ }
+ }
+
+
public virtual Absy! Label2Absy(string! label)
{
throw new System.NotImplementedException();
diff --git a/Source/VCGeneration/ConditionGeneration.ssc b/Source/VCGeneration/ConditionGeneration.ssc index 2129b1fb..9bfa56ab 100644 --- a/Source/VCGeneration/ConditionGeneration.ssc +++ b/Source/VCGeneration/ConditionGeneration.ssc @@ -120,6 +120,10 @@ namespace Microsoft.Boogie public virtual void OnUnreachableCode(Implementation! impl)
{
}
+
+ public virtual void OnWarning(string! msg)
+ {
+ }
}
}
diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc index bfdcf6c6..0644c14f 100644 --- a/Source/VCGeneration/VC.ssc +++ b/Source/VCGeneration/VC.ssc @@ -1704,6 +1704,11 @@ namespace VC {
resourceExceededMessage = msg;
}
+
+ public override void OnProverWarning(string! msg)
+ {
+ callback.OnWarning(msg);
+ }
}
public class ErrorReporterLocal : ErrorReporter {
|