diff --git a/src/main/scala/leon/TestGeneration.scala b/src/main/scala/leon/TestGeneration.scala index 14269dccc603ab0eae013ed125cc980d3b76830a..5a27d30b7292db35109c5d2aa29d8dfda197072f 100644 --- a/src/main/scala/leon/TestGeneration.scala +++ b/src/main/scala/leon/TestGeneration.scala @@ -25,7 +25,6 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) { case Waypoint(1, _) => true case _ => false })).get - println("Top level function: " + topFunDef) val testFun = new FunDef(FreshIdentifier("test"), UnitType, Seq()) val funInvocs = testcases.map(testcase => { @@ -39,7 +38,6 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) { FunctionInvocation(topFunDef, args) }).toSeq testFun.body = Some(Block(funInvocs, UnitLiteral)) - println("The test function:\n" + testFun) val Program(id, ObjectDef(objId, defs, invariants)) = program val testProgram = Program(id, ObjectDef(objId, testFun +: defs , invariants)) diff --git a/testcases/testgen/Diamond.scala b/testcases/testgen/Diamond.scala new file mode 100644 index 0000000000000000000000000000000000000000..dbd354e94ffe82de38d7a83997fa1553189f7c0b --- /dev/null +++ b/testcases/testgen/Diamond.scala @@ -0,0 +1,9 @@ +import leon.Utils._ + +object Diamond { + + def foo(x: Int): Int = waypoint(1, if(x < 0) bar(x) else bar(x)) + + def bar(y: Int): Int = if(y > 5) y else -y + +} diff --git a/testcases/testgen/MultiCall.scala b/testcases/testgen/MultiCall.scala new file mode 100644 index 0000000000000000000000000000000000000000..e536d275b86ef1c2f5989a3399c8d242d4d9ccfb --- /dev/null +++ b/testcases/testgen/MultiCall.scala @@ -0,0 +1,14 @@ +import leon.Utils._ + +object MultiCall { + + + def a(i: Int): Int = waypoint(1, if(i < 0) b(i) else c(i)) + + def b(j: Int): Int = if(j == -5) d(j) else e(j) + def c(k: Int): Int = if(k == 5) d(k) else e(k) + + def d(l: Int): Int = l + def e(m: Int): Int = m + +} diff --git a/testcases/testgen/Sum.scala b/testcases/testgen/Sum.scala new file mode 100644 index 0000000000000000000000000000000000000000..786b009808f86d6e6db3d9ef91f0820ee4d2a2c3 --- /dev/null +++ b/testcases/testgen/Sum.scala @@ -0,0 +1,9 @@ +import leon.Utils._ + +object Sum { + + def sum(n: Int): Int = { + waypoint(1, if(n <= 0) 0 else n + sum(n-1)) + } ensuring(_ >= 0) + +}