From ff1a4a32676fad3a78aad69d963f9f94bb07615c Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Mon, 17 Dec 2018 15:43:37 +0100
Subject: Added a simple postpass oracle that splits a bblock into single
 instruction bundles

---
 mppa_k1c/PostpassScheduling.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'mppa_k1c/PostpassScheduling.v')

diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
index 5232f903..1483a5d7 100644
--- a/mppa_k1c/PostpassScheduling.v
+++ b/mppa_k1c/PostpassScheduling.v
@@ -19,6 +19,8 @@ Local Open Scope error_monad_scope.
     returns a schedule expressed as a list of bundles *)
 Axiom schedule: bblock -> list bblock.
 
+Extract Constant schedule => "PostpassSchedulingOracle.schedule".
+
 (* TODO - implement the verificator *)
 Definition verified_schedule (bb : bblock) : res (list bblock) := OK (schedule bb).
 
-- 
cgit