diff --git a/src/main/scala/leon/CallGraph.scala b/src/main/scala/leon/testgen/CallGraph.scala similarity index 99% rename from src/main/scala/leon/CallGraph.scala rename to src/main/scala/leon/testgen/CallGraph.scala index f0c37c3c9056b9de27d4f977e024c06073acc89a..16e31057390e2cea0fd1714d7631c819593ecc04 100644 --- a/src/main/scala/leon/CallGraph.scala +++ b/src/main/scala/leon/testgen/CallGraph.scala @@ -1,9 +1,10 @@ -package leon +package leon.testgen import leon.purescala.Definitions._ import leon.purescala.Trees._ import leon.purescala.TypeTrees._ import leon.purescala.Common._ +import leon.FairZ3Solver class CallGraph(val program: Program) { diff --git a/src/main/scala/leon/TestGeneration.scala b/src/main/scala/leon/testgen/TestGeneration.scala similarity index 94% rename from src/main/scala/leon/TestGeneration.scala rename to src/main/scala/leon/testgen/TestGeneration.scala index 2935816eb9d80bd76bcf0371d3ceeba5cf62595d..1b48d72579f0ff620ef7d35f41e9bcfe841f3ac4 100644 --- a/src/main/scala/leon/TestGeneration.scala +++ b/src/main/scala/leon/testgen/TestGeneration.scala @@ -1,13 +1,15 @@ -package leon - -import purescala.Common._ -import purescala.Definitions._ -import purescala.Trees._ -import purescala.TypeTrees._ -import purescala.ScalaPrinter -import Extensions._ -import scala.collection.mutable.{Set => MutableSet} +package leon.testgen + +import leon.purescala.Common._ +import leon.purescala.Definitions._ +import leon.purescala.Trees._ +import leon.purescala.TypeTrees._ +import leon.purescala.ScalaPrinter +import leon.Extensions._ +import leon.FairZ3Solver +import leon.Reporter +import scala.collection.mutable.{Set => MutableSet} class TestGeneration(reporter: Reporter) extends Analyser(reporter) { diff --git a/testcases/testgen/Abs.scala b/testcases/testgen/Abs.scala index e9b0326f66cb771521663ec79c11d390d1a3debb..4aa8307c8ec3da1d9ff941994b084d8590ce3afc 100644 --- a/testcases/testgen/Abs.scala +++ b/testcases/testgen/Abs.scala @@ -1,9 +1,11 @@ import leon.Utils._ +import leon.Annotations._ object Abs { + @main def abs(x: Int): Int = { - waypoint(1, if(x < 0) -x else x) + if(x < 0) -x else x } ensuring(_ >= 0) }