From 604d34ebda1000662397c37b66dc77426f4bcde3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 17 May 2012 15:54:55 +0200
Subject: [PATCH] create a new program that contains the test function and
print it in scala format
---
src/main/scala/leon/TestGeneration.scala | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/TestGeneration.scala b/src/main/scala/leon/TestGeneration.scala
index ede34a20b..5b2f86946 100644
--- a/src/main/scala/leon/TestGeneration.scala
+++ b/src/main/scala/leon/TestGeneration.scala
@@ -4,6 +4,7 @@ import purescala.Common._
import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
+import purescala.ScalaPrinter
import Extensions._
import scala.collection.mutable.{Set => MutableSet}
@@ -37,9 +38,13 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
}
FunctionInvocation(topFunDef, args)
}).toSeq
- testFun.body = Some(Block(funInvocs.init, funInvocs.last))
+ 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))
+ println("New program:\n" + ScalaPrinter(testProgram))
+
reporter.info("Running from waypoint with the following testcases:\n")
reporter.info(testcases.mkString("\n"))
}
--
GitLab