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 /Source/VCGeneration | |
| parent | a4f2bf6414f35907ab135cc6723683fe632467c4 (diff) | |
Use callback mechanism to report prover warnings; do not just write them to stdout/stderr
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/Check.ssc | 18 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.ssc | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.ssc | 5 |
3 files changed, 27 insertions, 0 deletions
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 {
|