Fix bug where Visitors could not visit Requires or Ensures because

the StdDispatch method was missing on both Classes.

1 files changed, 8 insertions, 0 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index d6ac8754..d961eb3e 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2434,6 +2434,10 @@ namespace Microsoft.Boogie {
         tc.Error(this, "preconditions must be of type bool");

       }

     }

+

+    public override Absy StdDispatch(StandardVisitor visitor) {

+      return visitor.VisitRequires(this);

+    }

   }

 

   public class Ensures : Absy, IPotentialErrorNode {

@@ -2528,6 +2532,10 @@ namespace Microsoft.Boogie {
         tc.Error(this, "postconditions must be of type bool");

       }

     }

+

+    public override Absy StdDispatch(StandardVisitor visitor) {

+      return visitor.VisitEnsures(this);

+    }

   }

 

   public class Procedure : DeclWithFormals {