Added more tests and worked on adding support for "canned errors".

2 files changed, 14 insertions, 6 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 787477ad..abbcf4aa 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1527,16 +1527,15 @@ namespace VC {
           }

           else if (currentImplementation != null

                    && currentImplementation.AnyErrorsInCachedSnapshot

-                   && currentImplementation.InjectedAssumptionVariables != null

-                   && currentImplementation.InjectedAssumptionVariables.Any()

                    && ac.Checksum != null

                    && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))

                    && currentImplementation.ErrorChecksumsInCachedSnapshot.Contains(ac.Checksum)

-                   && !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v)))

+                   && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))

           {

-            ac.Attributes = new QKeyValue(Token.NoToken, "canned_failing_assertion", new List<object>(), ac.Attributes);

+            // TODO(wuestholz): Uncomment this once the canned errors are reported.

+            // pc = new AssumeCmd(ac.tok, copy);

+            pc.Attributes = new QKeyValue(Token.NoToken, "canned_failing_assertion", new List<object>(), pc.Attributes);

             currentImplementation.AddCannedFailingAssertion(ac);

-            // TODO(wuestholz): Turn the 'assert' command into an 'assume' command.

           }

         }

         else if (pc is AssumeCmd

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 505f18b7..9aa764e2 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1481,7 +1481,16 @@ namespace VC {
       ModelViewInfo mvInfo;

       var gotoCmdOrigins = PassifyImpl(impl, out mvInfo);

 

-      // TODO(wuestholz): Report all canned failing assertions for this implementation.

+      // Report all canned failing assertions for this implementation.

+      if (impl.CannedFailingAssertions != null)

+      {

+        foreach (var a in impl.CannedFailingAssertions)

+        {

+          // TODO(wuestholz): Implement this.

+          // var cex = AssertCmdToCounterexample(a, ...);

+          // callback.OnCounterexample(cex, ...);

+        }

+      }

 

       // If "expand" attribute is supplied, expand any assertion of conjunctions into multiple assertions, one per conjunct

       foreach (var b in impl.Blocks)