From 84bca4ab9cad8fb0bd67d78c79fd20a132709ae8 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 4 Apr 2013 15:22:09 +0200
Subject: [PATCH] Compile functions with their pre/post conditions
---
src/main/scala/leon/codegen/CodeGeneration.scala | 16 +++++++++++++++-
1 file changed, 15 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 0afef05bf..c436893e2 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -56,7 +56,21 @@ object CodeGeneration {
def compileFunDef(funDef : FunDef, ch : CodeHandler)(implicit env : CompilationEnvironment) {
val newMapping = funDef.args.map(_.id).zipWithIndex.toMap
- val exprToCompile = purescala.TreeOps.matchToIfThenElse(funDef.getBody)
+ val bodyWithPre = if(funDef.hasPrecondition) {
+ IfExpr(funDef.precondition.get, funDef.getBody, Error("Precondition failed"))
+ } else {
+ funDef.getBody
+ }
+
+ val bodyWithPost = if(funDef.hasPostcondition) {
+ val freshResID = FreshIdentifier("result").setType(funDef.returnType)
+ val post = purescala.TreeOps.replace(Map(ResultVariable() -> Variable(freshResID)), funDef.postcondition.get)
+ Let(freshResID, bodyWithPre, IfExpr(post, Variable(freshResID), Error("Postcondition failed")) )
+ } else {
+ bodyWithPre
+ }
+
+ val exprToCompile = purescala.TreeOps.matchToIfThenElse(bodyWithPost)
mkExpr(exprToCompile, ch)(env.withVars(newMapping))
--
GitLab