From e2a9013abd366b8145650aa8ee462d52681b3d68 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 20 Jun 2012 17:32:16 +0200
Subject: [PATCH] add annotation for main function
---
src/main/scala/leon/Annotations.scala | 1 +
src/main/scala/leon/TestGeneration.scala | 2 ++
src/main/scala/leon/plugin/CodeExtraction.scala | 1 +
3 files changed, 4 insertions(+)
diff --git a/src/main/scala/leon/Annotations.scala b/src/main/scala/leon/Annotations.scala
index 0831c8ff8..85e8c00e0 100644
--- a/src/main/scala/leon/Annotations.scala
+++ b/src/main/scala/leon/Annotations.scala
@@ -3,4 +3,5 @@ package leon
object Annotations {
class induct extends StaticAnnotation
class axiomatize extends StaticAnnotation
+ class main extends StaticAnnotation
}
diff --git a/src/main/scala/leon/TestGeneration.scala b/src/main/scala/leon/TestGeneration.scala
index 5a27d30b7..5aeb48714 100644
--- a/src/main/scala/leon/TestGeneration.scala
+++ b/src/main/scala/leon/TestGeneration.scala
@@ -19,6 +19,8 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
def analyse(program: Program) {
z3Solver.setProgram(program)
reporter.info("Running test generation")
+ program.definedFunctions.foreach(fd => println(fd.annotations))
+
val testcases = generateTestCases(program)
val topFunDef = program.definedFunctions.find(fd => fd.body.exists(body => body match {
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index b89dc39db..57aa0af64 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -203,6 +203,7 @@ trait CodeExtraction extends Extractors {
a.atp.safeToString match {
case "leon.Annotations.induct" => funDef.addAnnotation("induct")
case "leon.Annotations.axiomatize" => funDef.addAnnotation("axiomatize")
+ case "leon.Annotations.main" => funDef.addAnnotation("main")
case _ => ;
}
}
--
GitLab