From 8c1e56414da2326711efdda18fde7578cc78a373 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Mon, 25 May 2020 11:11:06 +0200
Subject: Adding stub RTLpathLivegenaux.ml

---
 Makefile.extr                     | 3 ++-
 mppa_k1c/lib/RTLpathLivegen.v     | 2 ++
 mppa_k1c/lib/RTLpathLivegenaux.ml | 4 ++++
 3 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 mppa_k1c/lib/RTLpathLivegenaux.ml

diff --git a/Makefile.extr b/Makefile.extr
index f2d06def..b131e84b 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -43,7 +43,8 @@ cparser/pre_parser_messages.ml:
 
 DIRS=extraction \
   lib common $(ARCH) backend cfrontend cparser driver \
-  exportclight debug mppa_k1c/unittest mppa_k1c/abstractbb/Impure/ocaml
+  exportclight debug mppa_k1c/unittest mppa_k1c/abstractbb/Impure/ocaml \
+  mppa_k1c/lib
 
 INCLUDES=$(patsubst %,-I %, $(DIRS))
 
diff --git a/mppa_k1c/lib/RTLpathLivegen.v b/mppa_k1c/lib/RTLpathLivegen.v
index 80df6e7c..4acd646f 100644
--- a/mppa_k1c/lib/RTLpathLivegen.v
+++ b/mppa_k1c/lib/RTLpathLivegen.v
@@ -18,6 +18,8 @@ Local Open Scope option_monad_scope.
 
 Axiom build_path_map: RTL.function -> path_map.
 
+Extract Constant build_path_map => "RTLpathLivegenaux.build_path_map".
+
 Fixpoint list_mem (rl: list reg) (alive: Regset.t) {struct rl}: bool :=
   match rl with
   | nil => true
diff --git a/mppa_k1c/lib/RTLpathLivegenaux.ml b/mppa_k1c/lib/RTLpathLivegenaux.ml
new file mode 100644
index 00000000..84ba345a
--- /dev/null
+++ b/mppa_k1c/lib/RTLpathLivegenaux.ml
@@ -0,0 +1,4 @@
+(* open RTLpath *)
+open Maps
+
+let build_path_map f = PTree.empty
-- 
cgit