From a5b1437bd1b1d1e8b934e2a0864e700370b7abdd Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 22 Apr 2016 18:43:13 +0200
Subject: [PATCH] extern never extracts the body
---
.../scala/leon/frontends/scalac/CodeExtraction.scala | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index dfab2acc8..b429f0ed5 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -941,11 +941,14 @@ trait CodeExtraction extends ASTExtractors {
NoTree(funDef.returnType)
}
- if (fctx.isExtern && !exists(_.isInstanceOf[NoTree])(finalBody)) {
- reporter.warning(finalBody.getPos, "External function could be extracted as Leon tree: "+finalBody)
- }
+ //if (fctx.isExtern && !exists(_.isInstanceOf[NoTree])(finalBody)) {
+ // reporter.warning(finalBody.getPos, "External function could be extracted as Leon tree: "+finalBody)
+ //}
funDef.fullBody = finalBody
+ if(fctx.isExtern) { //extern never keeps the body, but we keep pre and post
+ funDef.body = None
+ }
// Post-extraction sanity checks
--
GitLab