Henrique's addition to the the ErrorHandler API to retrieve models

2 files changed, 29 insertions, 0 deletions

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();

         }