Skip to content
Snippets Groups Projects
Commit cc60855a authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Duplicate programs to limit side-effects

parent 60d7be95
No related branches found
No related tags found
No related merge requests found
...@@ -65,6 +65,13 @@ object Definitions { ...@@ -65,6 +65,13 @@ object Definitions {
out.write(ScalaPrinter(this)) out.write(ScalaPrinter(this))
out.close out.close
} }
def duplicate = {
copy(mainObject = mainObject.copy(defs = mainObject.defs.collect {
case fd: FunDef => fd.duplicate
case d => d
}))
}
} }
object Program { object Program {
...@@ -278,6 +285,16 @@ object Definitions { ...@@ -278,6 +285,16 @@ object Definitions {
var parent: Option[FunDef] = None var parent: Option[FunDef] = None
var orig: Option[FunDef] = None var orig: Option[FunDef] = None
def duplicate: FunDef = {
val fd = new FunDef(id, returnType, args)
fd.body = body
fd.precondition = precondition
fd.postcondition = postcondition
fd.parent = parent
fd.orig = orig
fd
}
def hasImplementation : Boolean = body.isDefined def hasImplementation : Boolean = body.isDefined
def hasBody = hasImplementation def hasBody = hasImplementation
def hasPrecondition : Boolean = precondition.isDefined def hasPrecondition : Boolean = precondition.isDefined
......
...@@ -4,7 +4,8 @@ package termination ...@@ -4,7 +4,8 @@ package termination
import purescala.Definitions._ import purescala.Definitions._
import purescala.Trees._ import purescala.Trees._
class ComplexTerminationChecker(context: LeonContext, program: Program) extends TerminationChecker(context, program) { class ComplexTerminationChecker(context: LeonContext, _program: Program) extends TerminationChecker(context, _program.duplicate) {
import scala.collection.mutable.{Map => MutableMap} import scala.collection.mutable.{Map => MutableMap}
val name = "Complex Termination Checker" val name = "Complex Termination Checker"
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment