diff options
author | Pierre Goutagny <pierre.goutagny@ens-lyon.fr> | 2021-06-14 15:37:50 +0200 |
---|---|---|
committer | Pierre Goutagny <pierre.goutagny@ens-lyon.fr> | 2021-06-14 15:37:50 +0200 |
commit | 90375dc090b19cf8202903754d7f47e8d568d9f8 (patch) | |
tree | 0b98a0fa4c4588cd8a787d70f45b0468798beaf8 /backend/RTLTunneling.v | |
parent | 77d1ab5f7a6d04970185102508f1cec529c7cb40 (diff) | |
download | compcert-kvx-90375dc090b19cf8202903754d7f47e8d568d9f8.tar.gz compcert-kvx-90375dc090b19cf8202903754d7f47e8d568d9f8.zip |
Add RTL Tunneling as a pass
Diffstat (limited to 'backend/RTLTunneling.v')
-rw-r--r-- | backend/RTLTunneling.v | 1 |
1 files changed, 1 insertions, 0 deletions
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. |