aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Tunneling.v
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-06-10 18:28:26 +0200
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-06-10 18:28:26 +0200
commitf16fa31ec9cc90da750c8cc10f447023962cd153 (patch)
tree28eed4d4b5bc964907f20332d1eed470a393d07b /backend/Tunneling.v
parent485a4c0dd450e65745c83e59acdb40b42058e556 (diff)
parentd703ae1ad5e1fcdc63e07b2a50a3e8576a11e61e (diff)
downloadcompcert-kvx-f16fa31ec9cc90da750c8cc10f447023962cd153.tar.gz
compcert-kvx-f16fa31ec9cc90da750c8cc10f447023962cd153.zip
Merge branch 'kvx-work' into BTL
Diffstat (limited to 'backend/Tunneling.v')
-rw-r--r--backend/Tunneling.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/Tunneling.v b/backend/Tunneling.v
index 269ebb6f..c849ea92 100644
--- a/backend/Tunneling.v
+++ b/backend/Tunneling.v
@@ -34,8 +34,8 @@ Require Import LTL.
computations or useless moves), therefore there are more
opportunities for tunneling after allocation than before.
Symmetrically, prior tunneling helps linearization to produce
- better code, e.g. by revealing that some [nop] instructions are
- dead code (as the "nop L3" in the example above).
+ better code, e.g. by revealing that some [branch] instructions are
+ dead code (as the "branch L3" in the example above).
*)
(** The implementation consists in two passes: the first pass
@@ -51,7 +51,7 @@ Naively, we may define [branch_t f pc] as follows:
However, this definition can fail to terminate if
the program can contain loops consisting only of branches, as in
<<
- L1: nop L1;
+ L1: branch L1;
>>
or
<<