From aa4cc8d3121400e060bcbdc3ee1117c43273335e Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Mon, 27 Feb 2012 12:06:49 -0800
Subject: various fixes related to new error traces

---
 Source/VCGeneration/Check.cs | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'Source/VCGeneration/Check.cs')

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 9b7b6e36..73ca71b2 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -734,7 +734,11 @@ namespace Microsoft.Boogie {
       Undetermined
     }
     public class ErrorHandler {
-      public virtual void OnModel(IList<string>/*!>!*/ labels, ErrorModel errModel) {
+      public virtual void OnModel(Dictionary<int, IList<string>> labels, ErrorModel errModel) {
+
+      }
+
+      public virtual void OnModel(IList<string> labels, ErrorModel errModel) {
         Contract.Requires(cce.NonNullElements(labels));
       }
 
@@ -743,7 +747,6 @@ namespace Microsoft.Boogie {
       }
 
       public virtual void OnProverWarning(string message)
-        //modifies Console.Out.*, Console.Error.*;
       {
         Contract.Requires(message != null);
         switch (CommandLineOptions.Clo.PrintProverWarnings) {
@@ -761,7 +764,6 @@ namespace Microsoft.Boogie {
         }
       }
 
-
       public virtual Absy Label2Absy(string label) {
         Contract.Requires(label != null);
         Contract.Ensures(Contract.Result<Absy>() != null);
@@ -772,6 +774,9 @@ namespace Microsoft.Boogie {
     public abstract void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler);
     [NoDefaultContract]
     public abstract Outcome CheckOutcome(ErrorHandler handler);
+    public virtual Outcome CheckOutcome(ErrorHandler handler, IEnumerable<int> controlFlowConstants) {
+      throw new System.NotImplementedException();
+    }
     public virtual void LogComment(string comment) {
       Contract.Requires(comment != null);
     }
-- 
cgit v1.2.3