Skip to content
Snippets Groups Projects
Commit 676732cb authored by Régis Blanc's avatar Régis Blanc
Browse files

Merge branch 'develop' into testgen

parents 1b9c0d0c 4db2f838
Branches
Tags
No related merge requests found
...@@ -64,12 +64,14 @@ object FunctionClosure extends Pass { ...@@ -64,12 +64,14 @@ object FunctionClosure extends Pass {
newFunDef.postcondition = freshPostcondition newFunDef.postcondition = freshPostcondition
pathConstraints = fd.precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints pathConstraints = fd.precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints
val freshBody = fd.body.map(body => introduceLets(body, fd2FreshFd + (fd -> ((newFunDef, extraVarDeclFreshIds.map(_.toVariable)))))) //val freshBody = fd.body.map(body => introduceLets(body, fd2FreshFd + (fd -> ((newFunDef, extraVarDeclFreshIds.map(_.toVariable))))))
val freshBody = fd.body.map(body => introduceLets(body, fd2FreshFd + (fd -> ((newFunDef, extraVarDeclOldIds.map(_.toVariable))))))
newFunDef.body = freshBody newFunDef.body = freshBody
pathConstraints = pathConstraints.tail pathConstraints = pathConstraints.tail
val freshRest = functionClosure(rest, bindedVars, id2freshId, fd2FreshFd + (fd -> //val freshRest = functionClosure(rest, bindedVars, id2freshId, fd2FreshFd + (fd ->
((newFunDef, extraVarDeclOldIds.map(id => id2freshId.get(id).getOrElse(id).toVariable))))) // ((newFunDef, extraVarDeclOldIds.map(id => id2freshId.get(id).getOrElse(id).toVariable)))))
val freshRest = functionClosure(rest, bindedVars, id2freshId, fd2FreshFd + (fd -> ((newFunDef, extraVarDeclOldIds.map(_.toVariable)))))
freshRest.setType(l.getType) freshRest.setType(l.getType)
} }
case l @ Let(i,e,b) => { case l @ Let(i,e,b) => {
...@@ -99,7 +101,8 @@ object FunctionClosure extends Pass { ...@@ -99,7 +101,8 @@ object FunctionClosure extends Pass {
case fi @ FunctionInvocation(fd, args) => fd2FreshFd.get(fd) match { case fi @ FunctionInvocation(fd, args) => fd2FreshFd.get(fd) match {
case None => FunctionInvocation(fd, args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd))).setPosInfo(fi) case None => FunctionInvocation(fd, args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd))).setPosInfo(fi)
case Some((nfd, extraArgs)) => case Some((nfd, extraArgs)) =>
FunctionInvocation(nfd, args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd)) ++ extraArgs).setPosInfo(fi) FunctionInvocation(nfd, args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd)) ++
extraArgs.map(v => replace(id2freshId.map(p => (p._1.toVariable, p._2.toVariable)), v))).setPosInfo(fi)
} }
case n @ NAryOperator(args, recons) => { case n @ NAryOperator(args, recons) => {
val rargs = args.map(a => functionClosure(a, bindedVars, id2freshId, fd2FreshFd)) val rargs = args.map(a => functionClosure(a, bindedVars, id2freshId, fd2FreshFd))
...@@ -114,7 +117,7 @@ object FunctionClosure extends Pass { ...@@ -114,7 +117,7 @@ object FunctionClosure extends Pass {
val r = functionClosure(t, bindedVars, id2freshId, fd2FreshFd) val r = functionClosure(t, bindedVars, id2freshId, fd2FreshFd)
recons(r).setType(u.getType) recons(r).setType(u.getType)
} }
case m @ MatchExpr(scrut,cses) => { //still needs to handle the new ids introduced by the patterns case m @ MatchExpr(scrut,cses) => {
val scrutRec = functionClosure(scrut, bindedVars, id2freshId, fd2FreshFd) val scrutRec = functionClosure(scrut, bindedVars, id2freshId, fd2FreshFd)
val csesRec = cses.map{ val csesRec = cses.map{
case SimpleCase(pat, rhs) => { case SimpleCase(pat, rhs) => {
......
...@@ -1065,6 +1065,10 @@ trait CodeExtraction extends Extractors { ...@@ -1065,6 +1065,10 @@ trait CodeExtraction extends Extractors {
case LetVar(_, _, rest) => getReturnedExpr(rest) case LetVar(_, _, rest) => getReturnedExpr(rest)
case PBlock(_, rest) => getReturnedExpr(rest) case PBlock(_, rest) => getReturnedExpr(rest)
case IfExpr(_, then, elze) => getReturnedExpr(then) ++ getReturnedExpr(elze) case IfExpr(_, then, elze) => getReturnedExpr(then) ++ getReturnedExpr(elze)
case MatchExpr(_, cses) => cses.flatMap{
case SimpleCase(_, rhs) => getReturnedExpr(rhs)
case GuardedCase(_, _, rhs) => getReturnedExpr(rhs)
}
case _ => Seq(expr) case _ => Seq(expr)
} }
......
object Nested10 {
def foo(i: Int): Int = {
val n = 2
def rec1(j: Int) = {
i + j + n
}
def rec2(j: Int) = {
rec1(j)
}
rec2(2)
} ensuring(i + 4 == _)
}
object Nested11 {
abstract class A
case class B(b: Int) extends A
def foo(i: Int): Int = {
val b: A = B(3)
def rec1(j: Int) = b match {
case B(b) => i + j + b
}
rec1(2)
} ensuring(i + 5 == _)
}
object Nested12 {
abstract class A
case class B(b: Int) extends A
def foo(i: Int): Int = {
val b: A = B(3)
def rec1(a: A, j: Int, j2: Int) = a match {
case B(b) => i + j + j2 + b
}
def rec2(a: A, k: Int) = a match {
case B(b) => rec1(a, b, k)
}
rec2(b, 2)
} ensuring(i + 8 == _)
}
object Nested13 {
abstract class D
case class E(e: Int) extends D
case class F(d: D, f: Int) extends D
def foo(a : Int): Int = {
def rec1(d: D, j: Int): Int = d match {
case E(e) => j + e + a
case F(dNext, f) => f + rec1(dNext, j)
}
def rec2(d: D, i : Int) : Int = d match {
case E(e) => e
case F(dNext, f) => rec1(d, i)
}
rec2(F(E(2), 3), 0)
} ensuring(a + 5 == _)
}
object Nested14 {
def foo(i: Int): Int = {
def rec1(j: Int): Int = {
def rec2(k: Int): Int = if(k == 0) 0 else rec1(j-1)
rec2(j)
}
rec1(3)
} ensuring(0 == _)
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment