From 23dcb26351cf28a59d6a413194dff2d8faf6c591 Mon Sep 17 00:00:00 2001
From: stobies <unknown>
Date: Mon, 7 Sep 2009 11:19:08 +0000
Subject: Report prover warnings during smoke test via the VerifierCallback

---
 Source/VCGeneration/VC.ssc | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'Source/VCGeneration/VC.ssc')

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index 0644c14f..c0ebb933 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -564,7 +564,7 @@ namespace VC
           System.Console.WriteLine(" --- smoke #{0}, after passify", id);
           Emit();
         }
-        ch.BeginCheck((!) impl.Name + "_smoke" + id++, vc, new ErrorHandler(label2Absy));
+        ch.BeginCheck((!) impl.Name + "_smoke" + id++, vc, new ErrorHandler(label2Absy, this.callback));
         ch.ProverDone.WaitOne();
         ProverInterface.Outcome outcome = ch.ReadOutcome();
         parent.current_impl = null;
@@ -662,15 +662,21 @@ namespace VC
       
       class ErrorHandler : ProverInterface.ErrorHandler {
         Hashtable! label2Absy;
+        VerifierCallback! callback;
         
-        public ErrorHandler(Hashtable! label2Absy) {
+        public ErrorHandler(Hashtable! label2Absy, VerifierCallback! callback) {
           this.label2Absy = label2Absy;
+          this.callback = callback;
         }
         
         public override Absy! Label2Absy(string! label) {
           int id = int.Parse(label);
           return (Absy!) label2Absy[id];
         }
+        
+        public override void OnProverWarning(string! msg) {
+          this.callback.OnWarning(msg);
+        }
       }
     }
     
-- 
cgit v1.2.3