From 918ea1673b222dc251a3588de463d164dd3e4f4d Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Fri, 3 Sep 2010 21:14:04 +0000
Subject: Henrique's addition to the the ErrorHandler API to retrieve models

---
 Source/VCGeneration/ConditionGeneration.cs | 25 +++++++++++++++++++++++++
 Source/VCGeneration/VC.cs                  |  4 ++++
 2 files changed, 29 insertions(+)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index a99fb320..c7761a37 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -382,6 +382,8 @@ namespace VC {
     protected string/*?*/ logFilePath;
     protected bool appendLogFile;
 
+    public static List<ErrorModel> errorModelList;
+
     public ConditionGeneration(Program p) {
       Contract.Requires(p != null);
       program = p;
@@ -415,6 +417,29 @@ namespace VC {
       return outcome;
     }
 
+    /// <summary>
+    /// Takes an implementation and constructs a verification condition and sends
+    /// it to the theorem prover.
+    /// Returns null if "impl" is correct.  Otherwise, returns a list of counterexamples,
+    /// each counterexample consisting of an array of labels.
+    /// </summary>
+    /// <param name="impl"></param>
+    public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample> errors, out List<ErrorModel> errorsModel)
+    {
+        Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || errors != null);
+        Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+        List<Counterexample> errorsOut;
+
+        Outcome outcome;
+        errorModelList = new List<ErrorModel>();
+        outcome = VerifyImplementation(impl, program, out errorsOut);
+        errors = errorsOut;
+        errorsModel = errorModelList;
+
+        return outcome;
+    }
+  
+
     public Outcome StratifiedVerifyImplementation(Implementation impl, Program program, out List<Counterexample>/*?*/ errors) {
       Contract.Requires(impl != null);
       Contract.Requires(program != null);
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 68d34547..a906f137 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2909,6 +2909,10 @@ namespace VC {
       public override void OnModel(IList<string/*!*/>/*!*/ labels, ErrorModel errModel) {
         //Contract.Requires(cce.NonNullElements(labels));
         if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) {
+            if (VC.ConditionGeneration.errorModelList != null)
+            {
+                VC.ConditionGeneration.errorModelList.Add(errModel);
+            }
           errModel.Print(ErrorReporter.ModelWriter);
           ErrorReporter.ModelWriter.Flush();
         }
-- 
cgit v1.2.3