diff options
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 << |