Changed all lambda-expression rewriting to be done as a pre-processing step before real verification.

Fixed treatment of lambda-expression attributes.

1 files changed, 31 insertions, 5 deletions

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 98987c3f..d4be8ed4 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -297,7 +297,7 @@ namespace Microsoft.Boogie {
     }

     public virtual Expr VisitLambdaExpr(LambdaExpr node) {

       Contract.Requires(node != null);

-      Contract.Ensures(Contract.Result<LambdaExpr>() != null);

+      Contract.Ensures(Contract.Result<Expr>() != null);

       node = (LambdaExpr)this.VisitBinderExpr(node);

       return node;

     }

@@ -432,6 +432,20 @@ namespace Microsoft.Boogie {
       node.TopLevelDeclarations = this.VisitDeclarationList(node.TopLevelDeclarations);

       return node;

     }

+    public virtual QKeyValue VisitQKeyValue(QKeyValue node) {

+      Contract.Requires(node != null);

+      Contract.Ensures(Contract.Result<QKeyValue>() != null);

+      for (int i = 0, n = node.Params.Count; i < n; i++) {

+        var e = node.Params[i] as Expr;

+        if (e != null) {

+          node.Params[i] = (Expr)this.Visit(e);

+        }

+      }

+      if (node.Next != null) {

+        node.Next = (QKeyValue)this.Visit(node.Next);

+      }

+      return node;

+    }

     public virtual BinderExpr VisitBinderExpr(BinderExpr node) {

       Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<BinderExpr>() != null);

@@ -841,10 +855,9 @@ namespace Microsoft.Boogie {
           Contract.Ensures(Contract.Result<ForallExpr>() == node);

           return (ForallExpr)this.VisitQuantifierExpr(node);

       }

-      public override Expr VisitLambdaExpr(LambdaExpr node)

-      {

-          Contract.Ensures(Contract.Result<LambdaExpr>() == node);

-          return this.VisitBinderExpr(node);

+      public override Expr VisitLambdaExpr(LambdaExpr node) {

+        Contract.Ensures(Contract.Result<Expr>() == node);

+        return this.VisitBinderExpr(node);

       }

       public override Formal VisitFormal(Formal node)

       {

@@ -969,6 +982,19 @@ namespace Microsoft.Boogie {
           this.VisitDeclarationList(node.TopLevelDeclarations);

           return node;

       }

+      public override QKeyValue VisitQKeyValue(QKeyValue node) {

+        Contract.Ensures(Contract.Result<QKeyValue>() == node);

+        for (int i = 0, n = node.Params.Count; i < n; i++) {

+          var e = node.Params[i] as Expr;

+          if (e != null) {

+            this.Visit(e);

+          }

+        }

+        if (node.Next != null) {

+          this.Visit(node.Next);

+        }

+        return node;

+      }

       public override BinderExpr VisitBinderExpr(BinderExpr node)

       {

           Contract.Ensures(Contract.Result<BinderExpr>() == node);