diff --git a/src/main/scala/leon/TestGeneration.scala b/src/main/scala/leon/TestGeneration.scala index 5b2f86946294d80556ab1988c74b6c0918eae0e1..14269dccc603ab0eae013ed125cc980d3b76830a 100644 --- a/src/main/scala/leon/TestGeneration.scala +++ b/src/main/scala/leon/TestGeneration.scala @@ -43,7 +43,7 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) { val Program(id, ObjectDef(objId, defs, invariants)) = program val testProgram = Program(id, ObjectDef(objId, testFun +: defs , invariants)) - println("New program:\n" + ScalaPrinter(testProgram)) + testProgram.writeScalaFile("TestGen.scala") reporter.info("Running from waypoint with the following testcases:\n") reporter.info(testcases.mkString("\n")) diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala index bc497dcdd318cdbd7809c357b811002f986908da..3c18e858fcfeba8fa7d02421536e1080c5999847 100644 --- a/src/main/scala/leon/purescala/Definitions.scala +++ b/src/main/scala/leon/purescala/Definitions.scala @@ -54,6 +54,15 @@ object Definitions { def caseClassDef(name: String) = mainObject.caseClassDef(name) def allIdentifiers : Set[Identifier] = mainObject.allIdentifiers + id def isPure: Boolean = definedFunctions.forall(fd => fd.body.forall(Trees.isPure) && fd.precondition.forall(Trees.isPure) && fd.postcondition.forall(Trees.isPure)) + + def writeScalaFile(filename: String) { + import java.io.FileWriter + import java.io.BufferedWriter + val fstream = new FileWriter(filename) + val out = new BufferedWriter(fstream) + out.write(ScalaPrinter(this)) + out.close + } } /** Objects work as containers for class definitions, functions (def's) and