Worked on adding support for "canned errors".

1 files changed, 2 insertions, 0 deletions

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index be3ab95d..505f18b7 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1481,6 +1481,8 @@ namespace VC {
       ModelViewInfo mvInfo;

       var gotoCmdOrigins = PassifyImpl(impl, out mvInfo);

 

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

+

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

       foreach (var b in impl.Blocks)

       {