From 8f859490cd1241a13d29ca4f3c0e0dadb5aa7721 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 26 Apr 2012 21:05:51 +0200
Subject: [PATCH] Do not accept letdef in precondition and postcondition

---
 src/main/scala/leon/FunctionClosure.scala       |  5 +----
 src/main/scala/leon/plugin/CodeExtraction.scala | 10 ++++++++++
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index a180b1f16..d9426510e 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -72,14 +72,11 @@ object FunctionClosure extends Pass {
       val recBody = freshBody.map(b =>
                       functionClosure(b, bindedVars ++ newVarDecls.map(_.id))
                     ).map(b => searchAndReplaceDFS(substFunInvocInDef)(b))
-      val recPostcondition = freshPostcondition.map(expr =>
-                               functionClosure(expr, bindedVars ++ newVarDecls.map(_.id))
-                             ).map(expr => searchAndReplaceDFS(substFunInvocInDef)(expr))
       pathConstraints = oldPathConstraints
 
       newFunDef.precondition = recPrecondition
       newFunDef.body = recBody
-      newFunDef.postcondition = recPostcondition
+      newFunDef.postcondition = freshPostcondition
 
       def substFunInvocInRest(expr: Expr): Option[Expr] = expr match {
         case fi@FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ capturedVarsWithConstraints.map(_.toVariable)).setPosInfo(fi))
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 32e600e95..e54690c36 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -290,6 +290,11 @@ trait CodeExtraction extends Extractors {
           unit.error(realBody.pos, "Function precondtion should not contain nested function definition")
           throw ImpureCodeEncounteredException(realBody)
         })
+      ensCont.map(e => 
+        if(containsLetDef(e)) {
+          unit.error(realBody.pos, "Function postcondition should not contain nested function definition")
+          throw ImpureCodeEncounteredException(realBody)
+        })
       funDef.body = bodyAttempt
       funDef.precondition = reqCont
       funDef.postcondition = ensCont
@@ -440,6 +445,11 @@ trait CodeExtraction extends Extractors {
           unit.error(realBody.pos, "Function precondtion should not contain nested function definition")
           throw ImpureCodeEncounteredException(realBody)
         })
+      ensCont.map(e => 
+        if(containsLetDef(e)) {
+          unit.error(realBody.pos, "Function postcondition should not contain nested function definition")
+          throw ImpureCodeEncounteredException(realBody)
+        })
       funDef.body = bodyAttempt
       funDef.precondition = reqCont
       funDef.postcondition = ensCont
-- 
GitLab