diff --git a/library/lazy/package.scala b/library/lazy/package.scala
index f329b589abb38457cd8f53e1ebe15209c311f201..25dd1288d421ecf49d0136948b5392abae64c51b 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 14b8f5cdf5fb00237282ac231ed881b9179e053d..0e5aa269cf00234e08348064c512ebf35ac8a15c 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))