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

add annotation for main function

parent e981148d
No related branches found
No related tags found
No related merge requests found
...@@ -3,4 +3,5 @@ package leon ...@@ -3,4 +3,5 @@ package leon
object Annotations { object Annotations {
class induct extends StaticAnnotation class induct extends StaticAnnotation
class axiomatize extends StaticAnnotation class axiomatize extends StaticAnnotation
class main extends StaticAnnotation
} }
...@@ -19,6 +19,8 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) { ...@@ -19,6 +19,8 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
def analyse(program: Program) { def analyse(program: Program) {
z3Solver.setProgram(program) z3Solver.setProgram(program)
reporter.info("Running test generation") reporter.info("Running test generation")
program.definedFunctions.foreach(fd => println(fd.annotations))
val testcases = generateTestCases(program) val testcases = generateTestCases(program)
val topFunDef = program.definedFunctions.find(fd => fd.body.exists(body => body match { val topFunDef = program.definedFunctions.find(fd => fd.body.exists(body => body match {
......
...@@ -203,6 +203,7 @@ trait CodeExtraction extends Extractors { ...@@ -203,6 +203,7 @@ trait CodeExtraction extends Extractors {
a.atp.safeToString match { a.atp.safeToString match {
case "leon.Annotations.induct" => funDef.addAnnotation("induct") case "leon.Annotations.induct" => funDef.addAnnotation("induct")
case "leon.Annotations.axiomatize" => funDef.addAnnotation("axiomatize") case "leon.Annotations.axiomatize" => funDef.addAnnotation("axiomatize")
case "leon.Annotations.main" => funDef.addAnnotation("main")
case _ => ; case _ => ;
} }
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment