From a9f3fe621437b87467066225e9ed558cde755ff8 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Wed, 9 Apr 2014 13:19:56 +0200
Subject: [PATCH] Improve FunDef.duplicate. FunDef.copyContentFrom
---
src/main/scala/leon/purescala/Definitions.scala | 13 +++++++++----
src/main/scala/leon/purescala/MethodLifting.scala | 6 +-----
2 files changed, 10 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 32f21b0e7..e3ad66bef 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -212,10 +212,15 @@ object Definitions {
def duplicate: FunDef = {
val fd = new FunDef(id, tparams, returnType, params)
- fd.fullBody = fullBody
- fd.parent = parent
- fd.orig = orig
- fd
+ fd.copyContentFrom(this)
+ fd.copiedFrom(this)
+ }
+
+ def copyContentFrom(from : FunDef) {
+ this.fullBody = from.fullBody
+ this.parent = from.parent
+ this.orig = from.orig
+ this.addAnnotation(from.annotations.toSeq : _*)
}
def hasBody = body.isDefined
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index d329b2949..a390c96f6 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -30,12 +30,8 @@ object MethodLifting extends TransformationPhase {
val receiver = FreshIdentifier("$this").setType(recType).setPos(cd.id)
val nfd = new FunDef(id, ctParams ++ fd.tparams, fd.returnType, ValDef(receiver, recType) +: fd.params)
- nfd.postcondition = fd.postcondition
- nfd.precondition = fd.precondition
- nfd.body = fd.body
-
+ nfd.copyContentFrom(fd)
nfd.setPos(fd)
- nfd.addAnnotation(fd.annotations.toSeq : _*)
mdToFds += fd -> nfd
}
--
GitLab