diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-10 18:28:26 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-10 18:28:26 +0200 |
commit | f16fa31ec9cc90da750c8cc10f447023962cd153 (patch) | |
tree | 28eed4d4b5bc964907f20332d1eed470a393d07b /backend/Tunneling.v | |
parent | 485a4c0dd450e65745c83e59acdb40b42058e556 (diff) | |
parent | d703ae1ad5e1fcdc63e07b2a50a3e8576a11e61e (diff) | |
download | compcert-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.v | 6 |
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 << |