From 90375dc090b19cf8202903754d7f47e8d568d9f8 Mon Sep 17 00:00:00 2001 From: Pierre Goutagny Date: Mon, 14 Jun 2021 15:37:50 +0200 Subject: Add RTL Tunneling as a pass --- backend/RTLTunneling.v | 1 + 1 file changed, 1 insertion(+) (limited to 'backend/RTLTunneling.v') diff --git a/backend/RTLTunneling.v b/backend/RTLTunneling.v index e6901a9f..049160fd 100644 --- a/backend/RTLTunneling.v +++ b/backend/RTLTunneling.v @@ -25,6 +25,7 @@ Definition UF := PTree.t (node * Z). (* The oracle returns a map of "nop" node to their target with a distance (ie the number of the "nop" node on the path) to the target. *) Axiom branch_target: RTL.function -> UF. +Extract Constant branch_target => "RTLTunnelingaux.branch_target". (* TODO: add an extraction command to link branch_target with its implementation *) Local Open Scope error_monad_scope. -- cgit