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

create a new program that contains the test function and print it in scala format

parent f5b69e3f
No related branches found
No related tags found
No related merge requests found
...@@ -4,6 +4,7 @@ import purescala.Common._ ...@@ -4,6 +4,7 @@ import purescala.Common._
import purescala.Definitions._ import purescala.Definitions._
import purescala.Trees._ import purescala.Trees._
import purescala.TypeTrees._ import purescala.TypeTrees._
import purescala.ScalaPrinter
import Extensions._ import Extensions._
import scala.collection.mutable.{Set => MutableSet} import scala.collection.mutable.{Set => MutableSet}
...@@ -37,9 +38,13 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) { ...@@ -37,9 +38,13 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
} }
FunctionInvocation(topFunDef, args) FunctionInvocation(topFunDef, args)
}).toSeq }).toSeq
testFun.body = Some(Block(funInvocs.init, funInvocs.last)) testFun.body = Some(Block(funInvocs, UnitLiteral))
println("The test function:\n" + testFun) 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("Running from waypoint with the following testcases:\n")
reporter.info(testcases.mkString("\n")) reporter.info(testcases.mkString("\n"))
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment