Change "Tunneling" to "LTLTunneling" everywhere

To respect the symmetry between RTL- and LTL-Tunneling

10 files changed, 14 insertions, 14 deletions

diff --git a/Makefile b/Makefile
index 4900b165..05e4cbcd 100644
--- a/Makefile
+++ b/Makefile
@@ -143,7 +143,7 @@ BACKEND=\
   FirstNop.v FirstNopproof.v \
   Allnontrap.v Allnontrapproof.v \
   Allocation.v Allocationproof.v \
-  Tunneling.v Tunnelingproof.v \
+  LTLTunneling.v LTLTunnelingproof.v \
   RTLTunneling.v RTLTunnelingproof.v \
   Linear.v Lineartyping.v \
   Linearize.v Linearizeproof.v \
diff --git a/backend/Tunneling.v b/backend/LTLTunneling.v
index c849ea92..4b404724 100644
--- a/backend/Tunneling.v
+++ b/backend/LTLTunneling.v
@@ -77,7 +77,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: LTL.function -> UF. 
-Extract Constant branch_target => "Tunnelingaux.branch_target".
+Extract Constant branch_target => "LTLTunnelingaux.branch_target".
 
 Local Open Scope error_monad_scope.
 
diff --git a/backend/Tunnelingaux.ml b/backend/LTLTunnelingaux.ml
index d4b88a5d..c3b8cf82 100644
--- a/backend/Tunnelingaux.ml
+++ b/backend/LTLTunnelingaux.ml
@@ -15,7 +15,7 @@
 This file implements the [branch_target] oracle that identifies "nop" branches in a LTL function,
 and computes their target node with the distance (ie the number of cummulated nops) toward this target.
 
-See [Tunneling.v]
+See [LTLTunneling.v]
 
 *)
 
diff --git a/backend/Tunnelingproof.v b/backend/LTLTunnelingproof.v
index 3bc92f75..d36d3c76 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/LTLTunnelingproof.v
@@ -17,7 +17,7 @@ Require Import Coqlib Maps Errors.
 Require Import AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations LTL.
-Require Import Tunneling.
+Require Import LTLTunneling.
 
 Local Open Scope nat.
 
diff --git a/backend/RTLTunneling.v b/backend/RTLTunneling.v
index 049160fd..df663f48 100644
--- a/backend/RTLTunneling.v
+++ b/backend/RTLTunneling.v
@@ -19,7 +19,7 @@ Require Import Coqlib Maps Errors.
 Require Import AST.
 Require Import RTL.
 
-(* This is a port of tunneling for LTL. See Tunneling.v *)
+(* This is a port of tunneling for LTL. See LTLTunneling.v *)
 
 Definition UF := PTree.t (node * Z).
 
diff --git a/backend/Tunnelinglibs.ml b/backend/Tunnelinglibs.ml
index 1bb35f7a..7c826ba4 100644
--- a/backend/Tunnelinglibs.ml
+++ b/backend/Tunnelinglibs.ml
@@ -16,7 +16,7 @@
 This file implements the core functions of the tunneling passes, for both RTL
 and LTL, by using a simplified CFG as a transparent interface
 
-See [Tunneling.v] and [RTLTunneling.v]
+See [LTLTunneling.v] and [RTLTunneling.v]
 
 *)
 
diff --git a/doc/index-kvx.html b/doc/index-kvx.html
index 62afb423..daa4cdc4 100644
--- a/doc/index-kvx.html
+++ b/doc/index-kvx.html
@@ -315,10 +315,10 @@ This IR is generic over the processor, even if currently, only used for KVX.
 </TR>
 
 <TR valign="top">
-  <TD>Branch tunneling</TD>
+  <TD>(LTL) Branch tunneling</TD>
   <TD>LTL to LTL</TD>
-  <TD><A HREF="html/compcert.backend.Tunneling.html">Tunneling</A></TD>
-  <TD><A HREF="html/compcert.backend.Tunnelingproof.html">Tunnelingproof</A></TD>
+  <TD><A HREF="html/compcert.backend.LTLTunneling.html">LTLTunneling</A></TD>
+  <TD><A HREF="html/compcert.backend.LTLTunnelingproof.html">LTLTunnelingproof</A></TD>
 </TR>
 
 <TR valign="top">
diff --git a/doc/index.html b/doc/index.html
index c3912cb2..34b87924 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -270,10 +270,10 @@ code.
 </TR>
 
 <TR valign="top">
-  <TD>Branch tunneling</TD>
+  <TD>(LTL) Branch tunneling</TD>
   <TD>LTL to LTL</TD>
-  <TD><A HREF="html/compcert.backend.Tunneling.html">Tunneling</A></TD>
-  <TD><A HREF="html/compcert.backend.Tunnelingproof.html">Tunnelingproof</A></TD>
+  <TD><A HREF="html/compcert.backend.LTLTunneling.html">LTLTunneling</A></TD>
+  <TD><A HREF="html/compcert.backend.LTLTunnelingproof.html">LTLTunnelingproof</A></TD>
 </TR>
 
 <TR valign="top">
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand
index a751b232..952bed22 100644
--- a/driver/Compiler.vexpand
+++ b/driver/Compiler.vexpand
@@ -308,7 +308,7 @@ EXPAND_RTL_FORWARD_SIMULATIONS
   eapply compose_forward_simulations.
     eapply Allocationproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
-    eapply Tunnelingproof.transf_program_correct; eassumption.
+    eapply LTLTunnelingproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply Linearizeproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml
index 067f0e4b..e45f0617 100644
--- a/tools/compiler_expand.ml
+++ b/tools/compiler_expand.ml
@@ -58,7 +58,7 @@ let post_rtl_passes =
   PARTIAL, Always, Require, (Some "Prepass scheduling"), "RTLpathScheduler", Noprint;
   TOTAL, Always, Require,  (Some "Projection to RTL"), "RTLpath", (Print (Printf.sprintf "RTL %d" ((Array.length rtl_passes) + 1)));
   PARTIAL, Always, Require, (Some "Register allocation"), "Allocation", (Print "LTL 1");
-  PARTIAL, Always, Require, (Some "Branch tunneling"), "Tunneling", (Print "LTL 2");
+  PARTIAL, Always, Require, (Some "LTL Branch tunneling"), "LTLTunneling", (Print "LTL 2");
   PARTIAL, Always, Require, (Some "CFG linearization"), "Linearize", Noprint;
   TOTAL, Always, Require, (Some "Label cleanup"), "CleanupLabels", Noprint;
   PARTIAL, (Option "debug"), Require, (Some "Debugging info for local variables"), "Debugvar", Noprint;