From f5b69e3fba1842f173f84eac48ac3dee31419c88 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 17 May 2012 15:48:53 +0200
Subject: [PATCH] generate a function that run all tests
---
src/main/scala/leon/TestGeneration.scala | 21 +++++++++++++++++++++
1 file changed, 21 insertions(+)
diff --git a/src/main/scala/leon/TestGeneration.scala b/src/main/scala/leon/TestGeneration.scala
index 6a6172b22..ede34a20b 100644
--- a/src/main/scala/leon/TestGeneration.scala
+++ b/src/main/scala/leon/TestGeneration.scala
@@ -19,6 +19,27 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
z3Solver.setProgram(program)
reporter.info("Running test generation")
val testcases = generateTestCases(program)
+
+ val topFunDef = program.definedFunctions.find(fd => fd.body.exists(body => body match {
+ 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 => {
+ val params = topFunDef.args
+ val args = topFunDef.args.map{
+ case VarDecl(id, tpe) => testcase.get(id) match {
+ case Some(v) => v
+ case None => simplestValue(tpe)
+ }
+ }
+ FunctionInvocation(topFunDef, args)
+ }).toSeq
+ testFun.body = Some(Block(funInvocs.init, funInvocs.last))
+ println("The test function:\n" + testFun)
+
reporter.info("Running from waypoint with the following testcases:\n")
reporter.info(testcases.mkString("\n"))
}
--
GitLab