diff --git a/doc/library.rst b/doc/library.rst
index 0f76bce89e0bdfc1a2f95b61027c7bc300e895db..8708e5a743fc36d4e7e52cd196c2e52bc0d09b8e 100644
--- a/doc/library.rst
+++ b/doc/library.rst
@@ -46,13 +46,9 @@ which instruct Leon to handle some functions or objects in a specialized way.
| | including a function name in the ``--functions`` |
| | command line option. |
+-------------------+---------------------------------------------------+
-| ``@repair`` | (Currently unused) |
-+-------------------+---------------------------------------------------+
| ``@induct`` | Use the inductive tactic when generating |
| | verification conditions. |
+-------------------+---------------------------------------------------+
-| ``@extern`` | (Currently unused) |
-+-------------------+---------------------------------------------------+
| ``@ignore`` | Ignore this definition when extracting Leon trees.|
| | This annotation is useful to define functions |
| | that are not in Leon's language but will be |
diff --git a/library/annotation/package.scala b/library/annotation/package.scala
index 5782172b88cda5abfd876fe2bee4a619e7635499..db553a7056ea0dc13bce656df9ef5c1433a3f9aa 100644
--- a/library/annotation/package.scala
+++ b/library/annotation/package.scala
@@ -8,12 +8,8 @@ package object annotation {
@ignore
class library extends StaticAnnotation
@ignore
- class repair extends StaticAnnotation
- @ignore
class induct extends StaticAnnotation
@ignore
- class extern extends StaticAnnotation
- @ignore
class ignore extends StaticAnnotation
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 9e34f76b2b78990c74156004739ff6511067f608..3d89df12eeea67d12873af8d17734124d5d5be55 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -154,15 +154,13 @@ trait CodeExtraction extends ASTExtractors {
case class DefContext(
tparams: Map[Symbol, TypeParameter] = Map(),
vars: Map[Symbol, () => LeonExpr] = Map(),
- mutableVars: Map[Symbol, () => LeonExpr] = Map(),
- isExtern: Boolean = false
+ mutableVars: Map[Symbol, () => LeonExpr] = Map()
) {
def union(that: DefContext) = {
copy(this.tparams ++ that.tparams,
this.vars ++ that.vars,
- this.mutableVars ++ that.mutableVars,
- this.isExtern || that.isExtern)
+ this.mutableVars ++ that.mutableVars)
}
def isVariable(s: Symbol) = (vars contains s) || (mutableVars contains s)
@@ -183,10 +181,6 @@ trait CodeExtraction extends ASTExtractors {
def isIgnored(s: Symbol) = {
(annotationsOf(s) contains "ignore") || s.fullName.toString.endsWith(".main")
}
-
- def isExtern(s: Symbol) = {
- annotationsOf(s) contains "extern"
- }
def extractUnits: List[UnitDef] = {
try {
@@ -631,7 +625,7 @@ trait CodeExtraction extends ASTExtractors {
// Type params of the function itself
val tparams = extractTypeParams(sym.typeParams.map(_.tpe))
- val nctx = dctx.copy(tparams = dctx.tparams ++ tparams.toMap, isExtern = isExtern(sym))
+ val nctx = dctx.copy(tparams = dctx.tparams ++ tparams.toMap)
val newParams = sym.info.paramss.flatten.map{ sym =>
val ptpe = toPureScalaType(sym.tpe)(nctx, sym.pos)
@@ -659,7 +653,7 @@ trait CodeExtraction extends ASTExtractors {
private def defineFieldFunDef(sym : Symbol, isLazy : Boolean)(implicit dctx : DefContext) : FunDef = {
- val nctx = dctx.copy(tparams = dctx.tparams, isExtern = isExtern(sym))
+ val nctx = dctx.copy(tparams = dctx.tparams)
val returnType = toPureScalaType(sym.info.finalResultType)(nctx, sym.pos)
@@ -790,7 +784,7 @@ trait CodeExtraction extends ASTExtractors {
val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap
- extractFunBody(fd, params, body)(DefContext(tparamsMap, isExtern = isExtern(sym)))
+ extractFunBody(fd, params, body)(DefContext(tparamsMap))
case ExDefaultValueFunction(sym, tparams, params, _ ,_ , _, body) =>
// Default value functions
@@ -913,7 +907,6 @@ trait CodeExtraction extends ASTExtractors {
}
} catch {
case e: ImpureCodeEncounteredException =>
- if (!dctx.isExtern) {
e.emit()
//val pos = if (body0.pos == NoPosition) NoPosition else leonPosToScalaPos(body0.pos.source, funDef.getPos)
if (ctx.findOptionOrDefault(ExtractionPhase.optStrictCompilation)) {
@@ -921,10 +914,9 @@ trait CodeExtraction extends ASTExtractors {
} else {
reporter.warning(funDef.getPos, "Function "+funDef.id.name+" is not fully unavailable to Leon.")
}
- }
- funDef.addAnnotation("abstract")
- NoTree(funDef.returnType)
+ funDef.addAnnotation("abstract")
+ NoTree(funDef.returnType)
}
funDef.fullBody = finalBody
@@ -1055,12 +1047,7 @@ trait CodeExtraction extends ASTExtractors {
case ExEnsuredExpression(body, contract) =>
val post = extractTree(contract)
- val b = try {
- extractTree(body)
- } catch {
- case (e: ImpureCodeEncounteredException) if dctx.isExtern =>
- NoTree(toPureScalaType(current.tpe)(dctx, current.pos))
- }
+ val b = extractTree(body)
val closure = post.getType match {
case BooleanType =>
@@ -1075,12 +1062,7 @@ trait CodeExtraction extends ASTExtractors {
val resId = FreshIdentifier("holds", BooleanType).setPos(current.pos).setOwner(currentFunDef)
val post = Lambda(Seq(LeonValDef(resId)), Variable(resId)).setPos(current.pos)
- val b = try {
- extractTree(body)
- } catch {
- case (e: ImpureCodeEncounteredException) if dctx.isExtern =>
- NoTree(toPureScalaType(current.tpe)(dctx, current.pos))
- }
+ val b = extractTree(body)
Ensuring(b, post)
@@ -1095,12 +1077,7 @@ trait CodeExtraction extends ASTExtractors {
case ExRequiredExpression(contract) =>
val pre = extractTree(contract)
- val b = try {
- rest.map(extractTree).getOrElse(UnitLiteral())
- } catch {
- case (e: ImpureCodeEncounteredException) if dctx.isExtern =>
- NoTree(toPureScalaType(current.tpe)(dctx, current.pos))
- }
+ val b = rest.map(extractTree).getOrElse(UnitLiteral())
rest = None
@@ -1186,7 +1163,7 @@ trait CodeExtraction extends ASTExtractors {
fd.addAnnotation(annotationsOf(d.symbol).toSeq : _*)
- val newDctx = dctx.copy(tparams = dctx.tparams ++ tparamsMap, isExtern = isExtern(sym))
+ val newDctx = dctx.copy(tparams = dctx.tparams ++ tparamsMap)
val oldCurrentFunDef = currentFunDef
@@ -1879,15 +1856,7 @@ trait CodeExtraction extends ASTExtractors {
if (seenClasses contains sym) {
classDefToClassType(getClassDef(sym, NoPosition), tps)
} else {
- if (dctx.isExtern) {
- unknownsToTP.getOrElse(sym, {
- val tp = TypeParameter(FreshIdentifier(sym.name.toString, Untyped, true)) //FIXME
- unknownsToTP += sym -> tp
- tp
- })
- } else {
- outOfSubsetError(NoPosition, "Unknown class "+sym.fullName)
- }
+ outOfSubsetError(NoPosition, "Unknown class "+sym.fullName)
}
}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 392e87c7e893e47ce6e58bac0064e26bc5b2068f..c6a39924c7f5d289878f7403c346eb88e9ec3966 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -56,9 +56,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val defaultTactic = new DefaultTactic(vctx)
val inductionTactic = new InductionTactic(vctx)
- def excludeByDefault(fd: FunDef): Boolean = {
- (fd.annotations contains "verified") || (fd.annotations contains "library")
- }
+ def excludeByDefault(fd: FunDef): Boolean = fd.annotations contains "library"
val fdFilter = {
import OptionsHelpers._