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

1 files changed, 10 insertions, 1 deletions

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)