From f107f793afc6a263f0f25267f70c5d4756b4bb43 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Mon, 14 Mar 2016 14:33:40 +0100
Subject: [PATCH] @extern @library functions compiled with an error body.
Before the compilation would throw an exception, although the methods were
not meant to be run.
---
library/lazy/package.scala | 4 ++--
src/main/scala/leon/codegen/CodeGeneration.scala | 7 ++++++-
2 files changed, 8 insertions(+), 3 deletions(-)
diff --git a/library/lazy/package.scala b/library/lazy/package.scala
index f329b589a..25dd1288d 100644
--- a/library/lazy/package.scala
+++ b/library/lazy/package.scala
@@ -22,10 +22,10 @@ object $ {
* Should be used only in ensuring.
* TODO: enforce this.
*/
- @extern
+ @extern @library
def inState[T] : Set[$[T]] = sys.error("inState method is not executable!")
- @extern
+ @extern @library
def outState[T] : Set[$[T]] = sys.error("outState method is not executable")
/**
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 14b8f5cdf..0e5aa269c 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -200,7 +200,12 @@ trait CodeGeneration {
val body = if (params.checkContracts) {
funDef.fullBody
} else {
- funDef.body.getOrElse(throw CompilationException("Can't compile a FunDef without body: "+funDef.id.name))
+ funDef.body.getOrElse(
+ if(funDef.annotations contains "library") {
+ Error(funDef.id.getType, "Body of " + funDef.id.name + " not implemented at compile-time and still executed.")
+ } else {
+ throw CompilationException("Can't compile a FunDef without body: "+funDef.id.name)
+ })
}
val locals = NoLocals.withVars(newMapping).withTypes(funDef.tparams.map(_.tp))
--
GitLab