No-loop-initializers
The condition in which loop initialization blocks are empty.
The ForLoopInitRewriter transformation
moves the statements in each loop's initialization block
just before the loop.
This makes all the loop initialization blocks empty.
Here we formalize this condition,
which is needed to prove the correctness of certain transformations.
Subtopics
- Statements/blocks/cases/fundefs-noloopinitp
- Mutually recursive functions that check
the emptiness of loop initialization blocks in
statements, blocks, cases, and function definitions.
