From e2683e728976a6a6b22e2b97569155cbc3d576e7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 26 Apr 2012 19:54:35 +0200
Subject: [PATCH] keeping annotations while creating new FunDef
---
src/main/scala/leon/FunctionClosure.scala | 1 +
src/main/scala/leon/UnitElimination.scala | 4 ++++
2 files changed, 5 insertions(+)
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index 172281235..a180b1f16 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -52,6 +52,7 @@ object FunctionClosure extends Pass {
val newFunDef = new FunDef(newFunId, rt, newVarDecls).setPosInfo(fd)
newFunDef.fromLoop = fd.fromLoop
newFunDef.parent = fd.parent
+ newFunDef.addAnnotation(fd.annotations.toSeq:_*)
val freshPrecondition = precondition.map(expr => replace(freshVarsExpr, expr))
val freshPostcondition = postcondition.map(expr => replace(freshVarsExpr, expr))
diff --git a/src/main/scala/leon/UnitElimination.scala b/src/main/scala/leon/UnitElimination.scala
index 2f5f1bc53..2c5d4d5a5 100644
--- a/src/main/scala/leon/UnitElimination.scala
+++ b/src/main/scala/leon/UnitElimination.scala
@@ -24,6 +24,7 @@ object UnitElimination extends Pass {
freshFunDef.parent = fd.parent
freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
+ freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
fun2FreshFun += (fd -> freshFunDef)
} else {
fun2FreshFun += (fd -> fd) //this will make the next step simpler
@@ -97,6 +98,9 @@ object UnitElimination extends Pass {
else {
val (newFd, rest) = if(fd.args.exists(vd => vd.tpe == UnitType)) {
val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPosInfo(fd)
+ freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
+ freshFunDef.parent = fd.parent
+ freshFunDef.fromLoop = fd.fromLoop
freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
fun2FreshFun += (fd -> freshFunDef)
--
GitLab