From c00663415c37e89bbe7bbcea6ee5d9765662f1ed Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 17 May 2012 19:39:03 +0000
Subject: [PATCH] clean up the code
---
src/main/scala/leon/TestGeneration.scala | 2 --
testcases/testgen/Diamond.scala | 9 +++++++++
testcases/testgen/MultiCall.scala | 14 ++++++++++++++
testcases/testgen/Sum.scala | 9 +++++++++
4 files changed, 32 insertions(+), 2 deletions(-)
create mode 100644 testcases/testgen/Diamond.scala
create mode 100644 testcases/testgen/MultiCall.scala
create mode 100644 testcases/testgen/Sum.scala
diff --git a/src/main/scala/leon/TestGeneration.scala b/src/main/scala/leon/TestGeneration.scala
index 14269dccc..5a27d30b7 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 000000000..dbd354e94
--- /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 000000000..e536d275b
--- /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 000000000..786b00980
--- /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)
+
+}
--
GitLab