From fb017ac3f44122a65a6313e56265a8785326d58f Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 11 Jun 2015 23:55:13 +0200
Subject: [PATCH] Fix scalac compilation, accept non-specified @extern fundef

---
 library/collection/List.scala                             | 2 +-
 src/main/scala/leon/frontends/scalac/CodeExtraction.scala | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/collection/List.scala b/library/collection/List.scala
index daae8ef42..e2d0a1427 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -342,7 +342,7 @@ sealed abstract class List[T] {
 
   def rotate(s: BigInt): List[T] = {
     if (isEmpty) {
-      Nil()
+      Nil[T]()
     } else if (s < 0) {
       rotate(size+s)
     } else {
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index aa1e14430..0741d2b4b 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -896,7 +896,7 @@ trait CodeExtraction extends ASTExtractors {
         }} else body0
 
       val finalBody = try {
-        flattenBlocks(extractTree(body)(fctx)) match {
+        flattenBlocks(extractTreeOrNoTree(body)(fctx)) match {
           case e if e.getType.isInstanceOf[ArrayType] =>
             getOwner(e) match {
               case Some(Some(fd)) if fd == funDef =>
-- 
GitLab