diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index b3344d3476aec1a52029f455d4c6b93ee7b4a1ed..e4a84967021a60d73254b40e360c3fc0aa2457f8 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -191,15 +191,28 @@ trait ASTExtractors {
}
object ExCaseClass {
+ /*
+<<<<<<< HEAD
def unapply(cd: ClassDef): Option[(String,Symbol,Seq[(String, ValDef)], Template)] = cd match {
+=======
+ def unapply(cd: ClassDef): Option[(String,Symbol,Seq[(Symbol,Tree)], Template)] = cd match {
+>>>>>>> Field Extraction & handling
+*/
+ def unapply(cd: ClassDef): Option[(String,Symbol,Seq[(Symbol,ValDef)], Template)] = cd match {
case ClassDef(_, name, tparams, impl) if (cd.symbol.isCase && !cd.symbol.isAbstractClass && impl.body.size >= 8) => {
val constructor: DefDef = impl.children.find(child => child match {
case ExConstructorDef() => true
case _ => false
}).get.asInstanceOf[DefDef]
+/*
+<<<<<<< HEAD
val args = constructor.vparamss.flatten.map(vd => (vd.name.toString, vd))
-
+=======
+ val args = constructor.vparamss.flatten.map(vd => ( vd.symbol, vd.tpt))
+>>>>>>> Field Extraction & handling
+*/
+ val args = constructor.vparamss.flatten.map(vd => ( vd.symbol, vd))
Some((name.toString, cd.symbol, args, impl))
}
case _ => None
@@ -215,7 +228,7 @@ trait ASTExtractors {
}
}
}
-
+
object ExCaseClassSyntheticJunk {
def unapply(cd: ClassDef): Boolean = cd match {
case ClassDef(_, _, _, _) if (cd.symbol.isSynthetic) => true
@@ -240,14 +253,80 @@ trait ASTExtractors {
}
object ExFunctionDef {
- /** Matches a function with a single list of arguments, no type
- * parameters and regardless of its visibility. */
+ /** Matches a function with a single list of arguments,
+ * and regardless of its visibility.
+ */
def unapply(dd: DefDef): Option[(Symbol, Seq[Symbol], Seq[ValDef], Type, Tree)] = dd match {
- case DefDef(_, name, tparams, vparamss, tpt, rhs) if(name != nme.CONSTRUCTOR) =>
+ case DefDef(_, name, tparams, vparamss, tpt, rhs) if(
+ name != nme.CONSTRUCTOR && !dd.symbol.isSynthetic && !dd.symbol.isAccessor
+ ) =>
Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
case _ => None
}
}
+
+ object ExLazyAccessorFunction {
+ def unapply(dd: DefDef): Option[(Symbol, Type, Tree)] = dd match {
+ case DefDef(_, name, tparams, vparamss, tpt, rhs) if(
+ vparamss.size <= 1 && name != nme.CONSTRUCTOR &&
+ !dd.symbol.isSynthetic && dd.symbol.isAccessor && dd.symbol.isLazy
+ ) =>
+ Some((dd.symbol, tpt.tpe, rhs))
+ case _ => None
+ }
+ }
+
+ object ExFieldDef {
+ /** Matches a definition of a strict field inside a class constructor */
+ def unapply(vd : ValDef) : Option[(Symbol, Type, Tree)] = {
+ val sym = vd.symbol
+ vd match {
+ case ValDef(mods, name, tpt, rhs) if (
+ !sym.isCaseAccessor && !sym.isParamAccessor &&
+ !sym.isLazy && !sym.isSynthetic && !sym.isAccessor
+ ) =>
+ // Since scalac uses the accessor symbol all over the place, we pass that instead:
+ Some( (sym.getterIn(sym.owner),tpt.tpe,rhs) )
+ case _ => None
+ }
+ }
+ }
+
+ object ExLazyFieldDef {
+ /** Matches lazy field definitions.
+ * WARNING: Do NOT use this as extractor for lazy fields,
+ * as it does not contain the body of the lazy definition.
+ * It is here just to signify a Definition acceptable by Leon
+ */
+ def unapply(vd : ValDef) : Boolean = {
+ val sym = vd.symbol
+ vd match {
+ case ValDef(mods, name, tpt, rhs) if (
+ sym.isLazy && !sym.isCaseAccessor && !sym.isParamAccessor &&
+ !sym.isSynthetic && !sym.isAccessor
+ ) =>
+ // Since scalac uses the accessor symbol all over the place, we pass that instead:
+ true
+ case _ => false
+ }
+ }
+ }
+
+ object ExFieldAccessorFunction{
+ /** Matches the accessor function of a field
+ * WARNING: This is not meant to be used for any useful purpose,
+ * other than to satisfy Definition acceptable by Leon
+ */
+ def unapply(dd: DefDef): Boolean = dd match {
+ case DefDef(_, name, tparams, vparamss, tpt, rhs) if(
+ vparamss.size <= 1 && name != nme.CONSTRUCTOR &&
+ dd.symbol.isAccessor && !dd.symbol.isLazy
+ ) =>
+ true
+ case _ => false
+ }
+
+ }
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index a9502dff99494497a2fa72d76f7ac85dd1292f08..0b49d28fcffbd6eb073bc9cb209de02e3d74326f 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -106,12 +106,14 @@ trait CodeExtraction extends ASTExtractors {
}
class Extraction(units: List[CompilationUnit]) {
+
private var currentFunDef: FunDef = null
//This is a bit misleading, if an expr is not mapped then it has no owner, if it is mapped to None it means
//that it can have any owner
private var owners: Map[Identifier, Option[FunDef]] = Map()
+
def toPureScala(tree: Tree)(implicit dctx: DefContext): Option[LeonExpr] = {
try {
@@ -199,7 +201,7 @@ trait CodeExtraction extends ASTExtractors {
case d @ ExCaseClass(_, _, _, _) =>
standaloneDefs ::= d
None
-
+
case d @ ExCaseClassSyntheticJunk() =>
None
@@ -242,10 +244,9 @@ trait CodeExtraction extends ASTExtractors {
}
- private var seenClasses = Map[Symbol, (Seq[(String, ValDef)], Template)]()
+ private var seenClasses = Map[Symbol, (Seq[(Symbol, ValDef)], Template)]()
private var classesToClasses = Map[Symbol, LeonClassDef]()
-
def oracleType(pos: Position, tpe: LeonType) = {
classesToClasses.find {
case (sym, cl) => (sym.fullName.toString == "leon.lang.synthesis.Oracle")
@@ -323,7 +324,7 @@ trait CodeExtraction extends ASTExtractors {
private var isMethod = Set[Symbol]()
private var methodToClass = Map[FunDef, LeonClassDef]()
- def extractClassDef(sym: Symbol, args: Seq[(String, ValDef)], tmpl: Template): LeonClassDef = {
+ def extractClassDef(sym: Symbol, args: Seq[(Symbol, ValDef)], tmpl: Template): LeonClassDef = {
val id = FreshIdentifier(sym.name.toString).setPos(sym.pos)
val tparamsMap = sym.tpe match {
@@ -366,10 +367,10 @@ trait CodeExtraction extends ASTExtractors {
classesToClasses += sym -> ccd
- val fields = args.map { case (name, t) =>
+ val fields = args.map { case (symbol, t) =>
val tpt = t.tpt
val tpe = toPureScalaType(tpt.tpe)(defCtx, sym.pos)
- LeonValDef(FreshIdentifier(name).setType(tpe).setPos(t.pos), tpe).setPos(t.pos)
+ LeonValDef(FreshIdentifier(symbol.name.toString).setType(tpe).setPos(t.pos), tpe).setPos(t.pos)
}
ccd.setFields(fields)
@@ -397,7 +398,7 @@ trait CodeExtraction extends ASTExtractors {
ccd
}
- // We collect the methods
+ // We collect the methods and fields
for (d <- tmpl.body) d match {
case EmptyTree =>
// ignore
@@ -405,7 +406,8 @@ trait CodeExtraction extends ASTExtractors {
case t if isIgnored(t.symbol) =>
// ignore
- case t @ ExFunctionDef(fsym, _, _, _, _) if !fsym.isSynthetic && !fsym.isAccessor =>
+ // Normal methods
+ case t @ ExFunctionDef(fsym, _, _, _, _) =>
if (parent.isDefined) {
outOfSubsetError(t, "Only hierarchy roots can define methods")
}
@@ -416,6 +418,31 @@ trait CodeExtraction extends ASTExtractors {
cd.registerMethod(fd)
+ // Lazy fields
+ case t @ ExLazyAccessorFunction(fsym, _, _) =>
+ if (parent.isDefined) {
+ outOfSubsetError(t, "Only hierarchy roots can define lazy fields")
+ }
+ val fd = defineFieldFunDef(fsym, true)(defCtx)
+
+ isMethod += fsym
+ methodToClass += fd -> cd
+
+ cd.registerMethod(fd)
+
+ // normal fields
+ case t @ ExFieldDef(fsym, _, _) =>
+ // we will be using the accessor method of this field everywhere
+ val fsymAsMethod = fsym
+ if (parent.isDefined) {
+ outOfSubsetError(t, "Only hierarchy roots can define fields")
+ }
+ val fd = defineFieldFunDef(fsymAsMethod, false)(defCtx)
+
+ isMethod += fsymAsMethod
+ methodToClass += fd -> cd
+
+ cd.registerMethod(fd)
case _ =>
}
@@ -443,7 +470,7 @@ trait CodeExtraction extends ASTExtractors {
val name = sym.name.toString
- val fd = new FunDef(FreshIdentifier(name).setPos(sym.pos), tparamsDef, returnType, newParams)
+ val fd = new FunDef(FreshIdentifier(name).setPos(sym.pos), tparamsDef, returnType, newParams, DefType.MethodDef)
fd.setPos(sym.pos)
@@ -454,6 +481,29 @@ trait CodeExtraction extends ASTExtractors {
fd
}
+ private def defineFieldFunDef(sym : Symbol, isLazy : Boolean)(implicit dctx : DefContext) : FunDef = {
+
+ val nctx = dctx.copy(tparams = dctx.tparams, isExtern = isExtern(sym))
+
+ val returnType = toPureScalaType(sym.info.finalResultType)(nctx, sym.pos)
+
+ val name = sym.name.toString
+
+ val fieldType = if (isLazy) DefType.LazyFieldDef else DefType.StrictFieldDef
+
+ val fd = new FunDef(FreshIdentifier(name).setPos(sym.pos), Seq(), returnType, Seq(), fieldType)
+
+ fd.setPos(sym.pos)
+
+ fd.addAnnotation(annotationsOf(sym).toSeq : _*)
+
+ defsToDefs += sym -> fd
+
+ fd
+ }
+
+
+
private def collectFunSigs(defs: List[Tree]) = {
// We collect defined function bodies
for (d <- defs) d match {
@@ -463,6 +513,12 @@ trait CodeExtraction extends ASTExtractors {
case ExFunctionDef(sym, _, _, _, _) =>
defineFunDef(sym)(DefContext())
+ case ExLazyAccessorFunction(sym, _, _) =>
+ defineFieldFunDef(sym,true)(DefContext())
+
+ case ExFieldDef(sym, _, _) =>
+ defineFieldFunDef(sym, false)(DefContext())
+
case _ =>
}
}
@@ -482,7 +538,7 @@ trait CodeExtraction extends ASTExtractors {
val ctparamsMap = ctparams zip cd.tparams.map(_.tp)
for (d <- tmpl.body) d match {
- case ExFunctionDef(sym, tparams, params, _, body) if !sym.isSynthetic && !sym.isAccessor =>
+ case ExFunctionDef(sym, tparams, params, _, body) =>
val fd = defsToDefs(sym)
val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap ++ ctparamsMap
@@ -490,7 +546,23 @@ trait CodeExtraction extends ASTExtractors {
if(body != EmptyTree) {
extractFunBody(fd, params, body)(DefContext(tparamsMap))
}
-
+
+ // Lazy fields
+ case t @ ExLazyAccessorFunction(sym, _, body) =>
+ val fd = defsToDefs(sym)
+ val tparamsMap = ctparamsMap
+ if(body != EmptyTree) {
+ extractFunBody(fd, Seq(), body)(DefContext(tparamsMap.toMap))
+ }
+
+ // normal fields
+ case t @ ExFieldDef(sym, _, body) => // if !sym.isSynthetic && !sym.isAccessor =>
+ val fd = defsToDefs(sym)
+ val tparamsMap = ctparamsMap
+ if(body != EmptyTree) {
+ extractFunBody(fd, Seq(), body)(DefContext(tparamsMap.toMap))
+ }
+
case _ =>
}
@@ -515,13 +587,25 @@ trait CodeExtraction extends ASTExtractors {
case t if isIgnored(t.symbol) =>
// ignore
+
case ExFunctionDef(sym, tparams, params, _, body) =>
+ // Methods
val fd = defsToDefs(sym)
val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap
extractFunBody(fd, params, body)(DefContext(tparamsMap, isExtern = isExtern(sym)))
+ case ExLazyAccessorFunction(sym, _, body) =>
+ // Lazy vals
+ val fd = defsToDefs(sym)
+ extractFunBody(fd, Seq(), body)(DefContext())
+
+ case ExFieldDef(sym, tpe, body) =>
+ // Normal vals
+ val fd = defsToDefs(sym)
+ extractFunBody(fd, Seq(), body)(DefContext())
+
case _ =>
}
}
@@ -548,9 +632,14 @@ trait CodeExtraction extends ASTExtractors {
case ExCaseClass(o2, sym, args, _) =>
Some(classesToClasses(sym))
+ // Taking accessor functions will duplicate work for strict fields, but we need them in case of lazy fields
case ExFunctionDef(sym, tparams, params, _, body) =>
Some(defsToDefs(sym))
-
+ case ExLazyAccessorFunction(sym, _, _) =>
+ Some(defsToDefs(sym))
+ case ExFieldDef(sym, _, _) =>
+ Some(defsToDefs(sym))
+
case _ =>
None
}}
@@ -562,6 +651,10 @@ trait CodeExtraction extends ASTExtractors {
case ExCaseClass(_,_,_,_) =>
case ExConstructorDef() =>
case ExFunctionDef(_, _, _, _, _) =>
+ case ExLazyAccessorFunction(_, _, _) =>
+ case ExFieldDef(_,_,_) =>
+ case ExLazyFieldDef() =>
+ case ExFieldAccessorFunction() =>
case d if isIgnored(d.symbol) =>
case tree =>
outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");
@@ -571,9 +664,10 @@ trait CodeExtraction extends ASTExtractors {
}
- private def extractFunBody(funDef: FunDef, params: Seq[ValDef], body: Tree)(implicit dctx: DefContext): FunDef = {
+ private def extractFunBody(funDef: FunDef, params: Seq[ValDef], body0 : Tree)(implicit dctx: DefContext): FunDef = {
currentFunDef = funDef
-
+
+
val newVars = for ((s, vd) <- params zip funDef.params) yield {
s.symbol -> (() => Variable(vd.id))
}
@@ -581,6 +675,15 @@ trait CodeExtraction extends ASTExtractors {
val fctx = dctx.withNewVars(newVars)
+
+ // If this is a lazy field definition, drop the assignment/ accessing TODO
+ val body =
+ if (funDef.defType == DefType.LazyFieldDef) { body0 match {
+ case Block(List(Assign(_, realBody)),_ ) => realBody
+ case _ => outOfSubsetError(body0, "Wrong form of lazy accessor")
+ }} else body0
+
+
val finalBody = try {
flattenBlocks(extractTree(body)(fctx)) match {
case e if e.getType.isInstanceOf[ArrayType] =>
@@ -601,6 +704,7 @@ trait CodeExtraction extends ASTExtractors {
case e: ImpureCodeEncounteredException =>
if (!dctx.isExtern) {
e.emit()
+ //val pos = if (body0.pos == NoPosition) NoPosition else leonPosToScalaPos(body0.pos.source, funDef.getPos)
if (ctx.settings.strictCompilation) {
reporter.error(funDef.getPos, "Function "+funDef.id.name+" could not be extracted. (Forgot @extern ?)")
} else {
@@ -618,7 +722,7 @@ trait CodeExtraction extends ASTExtractors {
funDef.precondition.foreach { case e =>
if(containsLetDef(e)) {
- reporter.warning(e.getPos, "Function precondtion should not contain nested function definition, ignoring.")
+ reporter.warning(e.getPos, "Function precondition should not contain nested function definition, ignoring.")
funDef.precondition = None
}
}
@@ -1168,6 +1272,10 @@ trait CodeExtraction extends ASTExtractors {
val rargs = args.map(extractTree)
+ //println(s"symbol $sym with id ${sym.id}")
+ //println(s"isMethod($sym) == ${isMethod(sym)}")
+
+
(rrec, sym.name.decoded, rargs) match {
case (null, _, args) =>
val fd = getFunDef(sym, c.pos)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index e2d22bbb0c27235baffac9198e616bb53ecfd486..0bf35b4869a46fedf0ed5f8c85d68c23b350f9d9 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -209,9 +209,33 @@ object Definitions {
}
}
- /** Functions (= 'methods' of objects) */
- class FunDef(val id: Identifier, val tparams: Seq[TypeParameterDef], val returnType: TypeTree, val params: Seq[ValDef]) extends Definition {
-
+
+ // Definition types (see below)
+ object DefType extends Enumeration {
+ type DefType = Value
+ val MethodDef = Value("def")
+ val StrictFieldDef = Value("val")
+ val LazyFieldDef = Value("lazy val")
+ }
+ import DefType._
+
+ /** Functions
+ * This class represents methods or fields of objects (as specified by the defType field)
+ * that appear ONLY in the class/object's body (not the constructors)
+ * All of these are treated as functions for verification.
+ * Under circumstances (see canBeField and canBeLazyField methods)
+ * they can be differentiated when it comes to code generation/pretty printing.
+ *
+ * Default type is DefDef (method)
+ */
+ class FunDef(
+ val id: Identifier,
+ val tparams: Seq[TypeParameterDef],
+ val returnType: TypeTree,
+ val params: Seq[ValDef],
+ val defType : DefType
+ ) extends Definition {
+
var fullBody: Expr = NoTree(returnType)
def body: Option[Expr] = withoutSpec(fullBody)
@@ -234,7 +258,7 @@ object Definitions {
var orig: Option[FunDef] = None
def duplicate: FunDef = {
- val fd = new FunDef(id, tparams, returnType, params)
+ val fd = new FunDef(id, tparams, returnType, params, defType)
fd.copyContentFrom(this)
fd.copiedFrom(this)
}
@@ -251,6 +275,15 @@ object Definitions {
def hasPrecondition : Boolean = precondition.isDefined
def hasPostcondition : Boolean = postcondition.isDefined
+ /**
+ * When this functions has been annotated as a (lazy) field
+ * and has no arguments, it can be printed/compiled as a field
+ */
+ def canBeLazyField = defType == LazyFieldDef && params.isEmpty && tparams.isEmpty
+ def canBeStrictField = defType == StrictFieldDef && params.isEmpty && tparams.isEmpty
+ def canBeField = canBeLazyField || canBeStrictField
+ def isRealFunction = !canBeField
+
private var annots: Set[String] = Set.empty[String]
def addAnnotation(as: String*) : FunDef = {
annots = annots ++ as
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index f6b321365ba2ebaa301cf81c571f455f2d2b3864..8a4b6f6a5c9f3b8f691572106f1a754d3b963819 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -59,7 +59,7 @@ object FunctionClosure extends TransformationPhase {
val newBindedVars: Set[Identifier] = bindedVars ++ fd.params.map(_.id)
val newFunId = FreshIdentifier(fd.id.uniqueName) //since we hoist this at the top level, we need to make it a unique name
- val newFunDef = new FunDef(newFunId, fd.tparams, fd.returnType, newValDefs).copiedFrom(fd)
+ val newFunDef = new FunDef(newFunId, fd.tparams, fd.returnType, newValDefs, fd.defType).copiedFrom(fd)
topLevelFuns += newFunDef
newFunDef.addAnnotation(fd.annotations.toSeq:_*) //TODO: this is still some dangerous side effects
newFunDef.parent = Some(parent)
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index a390c96f64e2cbc7c675bbe115e91e31c4417d9a..f041559d3cad2c30db08e1ad2ad44d95b84a691b 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -29,7 +29,7 @@ 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)
+ val nfd = new FunDef(id, ctParams ++ fd.tparams, fd.returnType, ValDef(receiver, recType) +: fd.params, fd.defType)
nfd.copyContentFrom(fd)
nfd.setPos(fd)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 0d9b42aa9f87403461e5045570d4bba00b1d0776..9cc1baf3b8fb50b564cf38fc3cc88a3496b8ed88 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -240,7 +240,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
p"[${tfd.tps}]"
}
- p"($args)"
+ if (tfd.fd.isRealFunction) p"($args)"
case FunctionInvocation(tfd, args) =>
p"${tfd.id}"
@@ -249,7 +249,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
p"[${tfd.tps}]"
}
- p"($args)"
+ if (tfd.fd.isRealFunction) p"($args)"
case Plus(l,r) => optP { p"$l + $r" }
case Minus(l,r) => optP { p"$l - $r" }
@@ -431,8 +431,11 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
p"""|@$a
|"""
}
-
- if (!fd.tparams.isEmpty) {
+
+ if (fd.canBeField) {
+ p"""|${fd.defType} ${fd.id}: ${fd.returnType} = {
+ |"""
+ } else if (!fd.tparams.isEmpty) {
p"""|def ${fd.id}[${nary(fd.tparams, ",")}](${fd.params}): ${fd.returnType} = {
|"""
} else {
diff --git a/src/main/scala/leon/purescala/RestoreMethods.scala b/src/main/scala/leon/purescala/RestoreMethods.scala
index 43a53fe47b45c679fa9343438eaa80ff2295fc00..57f50ad4a0da0c85c3d5766cedee916934eb70d6 100644
--- a/src/main/scala/leon/purescala/RestoreMethods.scala
+++ b/src/main/scala/leon/purescala/RestoreMethods.scala
@@ -40,7 +40,8 @@ object RestoreMethods extends TransformationPhase {
id = FreshIdentifier(theName),
tparams = fn.tparams diff cd.tparams,
params = fn.params.tail, // no this$
- returnType = fn.returnType
+ returnType = fn.returnType,
+ defType = fn.defType
).copiedFrom(fn)
md.copyContentFrom(fn)
@@ -62,7 +63,7 @@ object RestoreMethods extends TransformationPhase {
val mi = MethodInvocation(
args.head, // "this"
args.head.getType.asInstanceOf[ClassType].classDef, // this.type
- md.typed(tfd.tps.takeRight(md.tparams.length)), // throw away class parameters
+ md.typed(tfd.tps.takeRight(md.tparams.length)), // throw away class type parameters
args.tail // rest of the arguments
)
Some(mi)
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index c72e6c3cee8cf077c5a14abc2794950b258d9b6c..91c6afd02ae9dac4e6b84cca577fbe921679094a 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -46,7 +46,7 @@ class ScopeSimplifier extends Transformer {
ValDef(newArg, tpe)
}
- val newFd = new FunDef(newId, fd.tparams, fd.returnType, newArgs)
+ val newFd = new FunDef(newId, fd.tparams, fd.returnType, newArgs, fd.defType)
newScope = newScope.registerFunDef(fd -> newFd)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index fef3caa93bc676880f1e5dd30b623059ee718c09..36c52c05935e82fa9a5674ab105a3b86c457c2b1 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1320,7 +1320,7 @@ object TreeOps {
val newFD = mapType(funDef.returnType) match {
case None => funDef
case Some(rt) =>
- val fd = new FunDef(FreshIdentifier(funDef.id.name, true), funDef.tparams, rt, funDef.params)
+ val fd = new FunDef(FreshIdentifier(funDef.id.name, true), funDef.tparams, rt, funDef.params, funDef.defType)
// These will be taken care of in the recursive traversal.
fd.body = funDef.body
fd.precondition = funDef.precondition
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index a77e0bd0cdaa66d49e155fb453b96e45aa913601..8841c2b94ce85e6c62b4abc13217642452402fb8 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -150,7 +150,7 @@ class UnrollingSolver(val context: LeonContext, underlyings: SolverFactory[Incre
private def getTemplate(body: Expr): FunctionTemplate = {
exprTemplateCache.getOrElse(body, {
- val fakeFunDef = new FunDef(FreshIdentifier("fake", true), Nil, body.getType, variablesOf(body).toSeq.map(id => ValDef(id, id.getType)))
+ val fakeFunDef = new FunDef(FreshIdentifier("fake", true), Nil, body.getType, variablesOf(body).toSeq.map(id => ValDef(id, id.getType)), DefType.MethodDef)
fakeFunDef.body = Some(body)
val res = FunctionTemplate.mkTemplate(fakeFunDef.typed, false)
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 2ec8bacff230378cccd6d7f1b7d31d96435355be..e220314d5bdfb387f3ff3581dd04ff4f8c9abb2f 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -146,7 +146,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
private def getTemplate(body: Expr): FunctionTemplate = {
exprTemplateCache.getOrElse(body, {
- val fakeFunDef = new FunDef(FreshIdentifier("fake", true), Nil, body.getType, variablesOf(body).toSeq.map(id => ValDef(id, id.getType)))
+ val fakeFunDef = new FunDef(FreshIdentifier("fake", true), Nil, body.getType, variablesOf(body).toSeq.map(id => ValDef(id, id.getType)), DefType.MethodDef)
fakeFunDef.body = Some(body)
val res = FunctionTemplate.mkTemplate(this, fakeFunDef.typed, false)
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index b069a1c738c1f6ae6deb331e4aed36b51f9e41ae..8f4ebf4ea526d97997f4d00cdf594c939a6f8ea5 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -127,7 +127,7 @@ class SimpleSearch(synth: Synthesizer,
Map(Variable(p.xs.head) -> res)
}
- val fd = new FunDef(FreshIdentifier("chimp", true), Nil, ret, freshAs.map(id => ValDef(id, id.getType)))
+ val fd = new FunDef(FreshIdentifier("chimp", true), Nil, ret, freshAs.map(id => ValDef(id, id.getType)),DefType.MethodDef)
fd.precondition = Some(replace(map, p.pc))
fd.postcondition = Some((res.id, replace(map++mapPost, p.phi)))
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 483dc9b36556630c3c2111fa1cb95297011c0d38..643855a771d1144a45cb8ddbadb020065e969c21 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -4,7 +4,7 @@ package leon
package synthesis
import purescala.Common._
-import purescala.Definitions.{Program, FunDef, ModuleDef}
+import purescala.Definitions.{Program, FunDef, ModuleDef, DefType}
import purescala.TreeOps._
import purescala.Trees._
import purescala.ScalaPrinter
@@ -112,7 +112,7 @@ class Synthesizer(val context : LeonContext,
Variable(id) -> TupleSelect(res, i+1)
}.toMap
- val fd = new FunDef(FreshIdentifier("finalTerm", true), Nil, ret, problem.as.map(id => ValDef(id, id.getType)))
+ val fd = new FunDef(FreshIdentifier("finalTerm", true), Nil, ret, problem.as.map(id => ValDef(id, id.getType)), DefType.MethodDef)
fd.precondition = Some(And(problem.pc, sol.pre))
fd.postcondition = Some((res.id, replace(mapPost, problem.phi)))
fd.body = Some(sol.term)
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index 87e4b14c854ce1ed66fe7aeceb5788da89ae24ee..d68cc347281790413914da88234b7f93b19914a4 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -77,7 +77,7 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
case sols =>
var globalPre = List[Expr]()
- val newFun = new FunDef(FreshIdentifier("rec", true), Nil, resType, ValDef(inductOn, inductOn.getType) +: residualArgDefs)
+ val newFun = new FunDef(FreshIdentifier("rec", true), Nil, resType, ValDef(inductOn, inductOn.getType) +: residualArgDefs, DefType.MethodDef)
val cases = for ((sol, (problem, pre, cct, ids, calls)) <- (sols zip subProblemsInfo)) yield {
globalPre ::= And(pre, sol.pre)
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
index 9c29ec85972fdf2ba7ed6257a1b5c49251b5d19b..ca9d99d88cf6a96a78964686f7ee7c6fa9a6d312 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
@@ -127,7 +127,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") with Heuristic {
case sols =>
var globalPre = List[Expr]()
- val newFun = new FunDef(FreshIdentifier("rec", true), Nil, resType, ValDef(inductOn, inductOn.getType) +: residualArgDefs)
+ val newFun = new FunDef(FreshIdentifier("rec", true), Nil, resType, ValDef(inductOn, inductOn.getType) +: residualArgDefs, DefType.MethodDef)
val cases = for ((sol, (problem, pat, calls, pc)) <- (sols zip subProblemsInfo)) yield {
globalPre ::= And(pc, sol.pre)
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index 37cf77a0ba97c679144b62a74482d4dbb1d0c759..bf98b7fcad1e93633b2a99e893981135e611fdff 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -44,7 +44,7 @@ case object IntInduction extends Rule("Int Induction") with Heuristic {
And(LessThan(Variable(inductOn), IntLiteral(0)), lt.pre)))
val preOut = subst(inductOn -> Variable(origId), preIn)
- val newFun = new FunDef(FreshIdentifier("rec", true), Nil, tpe, Seq(ValDef(inductOn, inductOn.getType)))
+ val newFun = new FunDef(FreshIdentifier("rec", true), Nil, tpe, Seq(ValDef(inductOn, inductOn.getType)),DefType.MethodDef)
val idPost = FreshIdentifier("res").setType(tpe)
newFun.precondition = Some(preIn)
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index d7dc070b73ae6face3f652a9181fac5c1125cd88..7cae2a7356ae5f967e5f7e687767995f9f5e513f 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -95,7 +95,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
//define max function
val maxValDefs: Seq[ValDef] = lowerBounds.map(_ => ValDef(FreshIdentifier("b"), Int32Type))
- val maxFun = new FunDef(FreshIdentifier("max"), Nil, Int32Type, maxValDefs)
+ val maxFun = new FunDef(FreshIdentifier("max"), Nil, Int32Type, maxValDefs, DefType.MethodDef)
def maxRec(bounds: List[Expr]): Expr = bounds match {
case (x1 :: x2 :: xs) => {
val v = FreshIdentifier("m").setType(Int32Type)
@@ -109,7 +109,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
def max(xs: Seq[Expr]): Expr = FunctionInvocation(maxFun.typed, xs)
//define min function
val minValDefs: Seq[ValDef] = upperBounds.map(_ => ValDef(FreshIdentifier("b"), Int32Type))
- val minFun = new FunDef(FreshIdentifier("min"), Nil, Int32Type, minValDefs)
+ val minFun = new FunDef(FreshIdentifier("min"), Nil, Int32Type, minValDefs,DefType.MethodDef)
def minRec(bounds: List[Expr]): Expr = bounds match {
case (x1 :: x2 :: xs) => {
val v = FreshIdentifier("m").setType(Int32Type)
@@ -123,10 +123,12 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
def min(xs: Seq[Expr]): Expr = FunctionInvocation(minFun.typed, xs)
val floorFun = new FunDef(FreshIdentifier("floorDiv"), Nil, Int32Type, Seq(
ValDef(FreshIdentifier("x"), Int32Type),
- ValDef(FreshIdentifier("x"), Int32Type)))
+ ValDef(FreshIdentifier("x"), Int32Type)),
+ DefType.MethodDef)
val ceilingFun = new FunDef(FreshIdentifier("ceilingDiv"), Nil, Int32Type, Seq(
ValDef(FreshIdentifier("x"), Int32Type),
- ValDef(FreshIdentifier("x"), Int32Type)))
+ ValDef(FreshIdentifier("x"), Int32Type)),
+ DefType.MethodDef)
ceilingFun.body = Some(IntLiteral(0))
def floorDiv(x: Expr, y: Expr): Expr = FunctionInvocation(floorFun.typed, Seq(x, y))
def ceilingDiv(x: Expr, y: Expr): Expr = FunctionInvocation(ceilingFun.typed, Seq(x, y))
@@ -192,7 +194,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
val concretePre = replace(Map(Variable(k) -> loopCounter), pre)
val concreteTerm = replace(Map(Variable(k) -> loopCounter), term)
val returnType = TupleType(problem.xs.map(_.getType))
- val funDef = new FunDef(FreshIdentifier("rec", true), Nil, returnType, Seq(ValDef(loopCounter.id, Int32Type)))
+ val funDef = new FunDef(FreshIdentifier("rec", true), Nil, returnType, Seq(ValDef(loopCounter.id, Int32Type)),DefType.MethodDef)
val funBody = expandAndSimplifyArithmetic(IfExpr(
LessThan(loopCounter, IntLiteral(0)),
Error("No solution exists"),
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index a6f22150082fdaf0f098fee04e4dd376ebc5abda..e9753151be1574a174e7530880af59e0fb38da2a 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -33,7 +33,7 @@ trait StructuralSize {
case None =>
val argument = ValDef(FreshIdentifier("x").setType(argumentType), argumentType)
val formalTParams = typeParams.map(TypeParameterDef(_))
- val fd = new FunDef(FreshIdentifier("size", true), formalTParams, Int32Type, Seq(argument))
+ val fd = new FunDef(FreshIdentifier("size", true), formalTParams, Int32Type, Seq(argument), DefType.MethodDef)
sizeCache(argumentType) = fd
val body = simplifyLets(matchToIfThenElse(MatchExpr(argument.toVariable, cases(argumentType))))
diff --git a/src/main/scala/leon/utils/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
index 4887bb18f3a09cf2c4ff5def5769faef14e53a0a..1c67c8f165eee6d4c2a4893dee068e9a601fb3f5 100644
--- a/src/main/scala/leon/utils/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -26,7 +26,7 @@ object UnitElimination extends TransformationPhase {
//first introduce new signatures without Unit parameters
allFuns.foreach(fd => {
if(fd.returnType != UnitType && fd.params.exists(vd => vd.tpe == UnitType)) {
- val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.returnType, fd.params.filterNot(vd => vd.tpe == UnitType)).setPos(fd)
+ val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.returnType, fd.params.filterNot(vd => vd.tpe == UnitType), fd.defType).setPos(fd)
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:_*)
@@ -104,7 +104,7 @@ object UnitElimination extends TransformationPhase {
removeUnit(b)
else {
val (newFd, rest) = if(fd.params.exists(vd => vd.tpe == UnitType)) {
- val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.returnType, fd.params.filterNot(vd => vd.tpe == UnitType)).setPos(fd)
+ val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.returnType, fd.params.filterNot(vd => vd.tpe == UnitType), fd.defType).setPos(fd)
freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
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..
diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index 7aa27b31792cb25015fe9f15a61d359da6b16ec6..e77030ab0da1903d91ccf14f4e76ebdd70613eb3 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -23,7 +23,7 @@ object EpsilonElimination extends TransformationPhase {
val newBody = postMap{
case eps@Epsilon(pred) =>
val freshName = FreshIdentifier("epsilon")
- val newFunDef = new FunDef(freshName, Nil, eps.getType, Seq())
+ val newFunDef = new FunDef(freshName, Nil, eps.getType, Seq(), DefType.MethodDef)
val epsilonVar = EpsilonVariable(eps.getPos)
val resId = FreshIdentifier("res").setType(eps.getType)
val postcondition = replace(Map(epsilonVar -> Variable(resId)), pred)
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index d94330d7ea4f429a45d5a44b769b11eab0111ea5..39334e495cb8d2ab54839a9fb93fd4c4f8299aeb 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -156,7 +156,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
val modifiedVars2WhileFunVars = modifiedVars.zip(whileFunVars).toMap
val whileFunValDefs = whileFunVars.map(id => ValDef(id, id.getType))
val whileFunReturnType = if(whileFunVars.size == 1) whileFunVars.head.getType else TupleType(whileFunVars.map(_.getType))
- val whileFunDef = new FunDef(FreshIdentifier(parent.id.name), Nil, whileFunReturnType, whileFunValDefs).setPos(wh)
+ val whileFunDef = new FunDef(FreshIdentifier(parent.id.name), Nil, whileFunReturnType, whileFunValDefs,DefType.MethodDef).setPos(wh)
wasLoop += whileFunDef
val whileFunCond = condRes
diff --git a/src/test/resources/regression/frontends/Fields.scala b/src/test/resources/regression/frontends/Fields.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b6e70e1ae1a32ada704c69e88a9799e212f77169
--- /dev/null
+++ b/src/test/resources/regression/frontends/Fields.scala
@@ -0,0 +1,29 @@
+import leon._
+import leon.lang._
+
+object Fields {
+ case class Cl(x : Int) {
+ lazy val lzy = x + 1
+
+ val eager = x + 2
+
+ def apply(y : Int) : Int = {
+ eager + lzy + y
+ } ensuring { _ == (2 * x + 3) + y }
+
+ }
+
+ def foo() : Int = {
+ 42
+ }
+
+ lazy val ox = 42
+
+ val oy = ox + 12
+
+ def lemma(cl : Cl) : Boolean = {
+ cl.eager + cl.lzy > 2 * cl.x
+ } holds
+}
+
+
diff --git a/src/test/scala/leon/test/frontends/FrontEndsTest.scala b/src/test/scala/leon/test/frontends/FrontEndsTest.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5c1ebd02b8afe7fe278f3fbc82968d561acdfd79
--- /dev/null
+++ b/src/test/scala/leon/test/frontends/FrontEndsTest.scala
@@ -0,0 +1,69 @@
+package leon.test.frontends
+
+import leon._
+import java.io.File
+
+class FrontEndsTest extends leon.test.LeonTestSuite {
+
+ val inputFilePath = "frontends"
+ val outputFilePath = "frontends"
+
+ private def forEachFileIn(path : String)(block : File => Unit) {
+ val fs = filesInResourceDir(path, _.endsWith(".scala"))
+
+ for(f <- fs) {
+ block(f)
+ }
+ }
+
+ val pipeline1 =
+ frontends.scalac.ExtractionPhase andThen
+ utils.ScopingPhase andThen
+ purescala.MethodLifting andThen
+ utils.TypingPhase andThen
+ purescala.CompleteAbstractDefinitions andThen
+ utils.FileOutputPhase
+
+ val pipeline2 =
+ frontends.scalac.ExtractionPhase andThen
+ utils.ScopingPhase andThen
+ purescala.MethodLifting andThen
+ utils.TypingPhase andThen
+ purescala.CompleteAbstractDefinitions andThen
+ purescala.RestoreMethods andThen
+ utils.FileOutputPhase
+
+ forEachFileIn(inputFilePath ) { f =>
+ testExtr(f)
+ }
+
+ def testExtr(f : File) {
+ val outFileName1 = outputDirHard(outputFilePath).getAbsolutePath() ++ "/" ++ f.getName
+ val outFileName2 = outputDirHard(outputFilePath).getAbsolutePath() ++ "/restored" ++ f.getName
+ test ("Testing " + f.getName) {
+ // Compile original file
+ val timeOut = 2
+ val settings = testContext.settings.copy(
+ debugSections = Set(),
+ injectLibrary = false //true
+ )
+ val ctx1 = testContext.copy(
+ // We want a reporter that actually prints some output
+ reporter = new DefaultReporter(settings),
+ settings = settings,
+ options = testContext.options :+ LeonValueOption("o", outFileName1) //:+ LeonFlagOption("library", true)
+ )
+
+ val ctx2 = ctx1.copy(
+ reporter = new DefaultReporter(settings),
+ settings = settings,
+ options = testContext.options :+ LeonValueOption("o", outFileName2 ) //:+ LeonFlagOption("library", true)
+ )
+
+ pipeline1.run(ctx1)(List(f.getAbsolutePath()))
+ pipeline2.run(ctx2)(List(f.getAbsolutePath()))
+
+ }
+
+ }
+}
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index 7ed2aa9bd46fe71affe48441f6478018584615f4..c0ab6eadba1465a232eff3c062b5d242b4039d1e 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -39,7 +39,7 @@ class FairZ3SolverTests extends LeonTestSuite {
// def f(fx : Int) : Int = fx + 1
private val fx : Identifier = FreshIdentifier("x").setType(Int32Type)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, Int32Type, ValDef(fx, Int32Type) :: Nil)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, Int32Type, ValDef(fx, Int32Type) :: Nil, DefType.MethodDef)
fDef.body = Some(Plus(Variable(fx), IntLiteral(1)))
private val minimalProgram = Program(
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
index 7f489e729b20cd549821778fe2534ee434bc79c2..b10a84d80d064a1fdf0453bfcb839bb2537d99a1 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -47,7 +47,7 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
// def f(fx : Int) : Int = fx + 1
private val fx : Identifier = FreshIdentifier("x").setType(Int32Type)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, Int32Type, ValDef(fx, Int32Type) :: Nil)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, Int32Type, ValDef(fx, Int32Type) :: Nil, DefType.MethodDef)
fDef.body = Some(Plus(Variable(fx), IntLiteral(1)))
private val minimalProgram = Program(
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index a0579dbd460a4c2589068e0dd5f03aa0c72a6ae4..2fb9909c4e9dee24992a95628ddead0e570b751a 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -40,11 +40,11 @@ class UninterpretedZ3SolverTests extends LeonTestSuite {
// def f(fx : Int) : Int = fx + 1
private val fx : Identifier = FreshIdentifier("x").setType(Int32Type)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, Int32Type, ValDef(fx, Int32Type) :: Nil)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, Int32Type, ValDef(fx, Int32Type) :: Nil, DefType.MethodDef)
fDef.body = Some(Plus(Variable(fx), IntLiteral(1)))
// g is a function that is not in the program (on purpose)
- private val gDef : FunDef = new FunDef(FreshIdentifier("g"), Nil, Int32Type, ValDef(fx, Int32Type) :: Nil)
+ private val gDef : FunDef = new FunDef(FreshIdentifier("g"), Nil, Int32Type, ValDef(fx, Int32Type) :: Nil, DefType.MethodDef)
gDef.body = Some(Plus(Variable(fx), IntLiteral(1)))
private val minimalProgram = Program(