From 5a5d3d932a282d36195653956cf1d539b92e9c97 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Wed, 16 Mar 2016 10:09:20 +0100
Subject: [PATCH] More permissive use of @extern without library so that the
body is compiled but not directly executable.
---
library/lazy/package.scala | 4 ++--
src/main/scala/leon/codegen/CodeGeneration.scala | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/library/lazy/package.scala b/library/lazy/package.scala
index 25dd1288d..f329b589a 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 @library
+ @extern
def inState[T] : Set[$[T]] = sys.error("inState method is not executable!")
- @extern @library
+ @extern
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 0e5aa269c..a33ec69e5 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -201,7 +201,7 @@ trait CodeGeneration {
funDef.fullBody
} else {
funDef.body.getOrElse(
- if(funDef.annotations contains "library") {
+ if(funDef.annotations contains "extern") {
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)
--
GitLab