Checks and enforces normal form properties for natural loops of the given goto_program.

If and when the function succeeds, the following properties are established for each natural loop.

The loop has either a single instruction:

OR

The loop has two or more instructions and:

1. has a unique head instruction;
2. has a unique, unconditional GOTO latch instruction;
3. has a pre-head SKIP instruction that is not part of the loop;
4. the head has two incoming edges from the pre-head and the latch;
5. for all instructions but the head, incoming edges are from instructions in the same loop;
6. all instructions of the loop are found between the head and the latch in the instruction sequence;
7. The span of instructions of any two loops are either nested or disjoint.

Remarks

The goto program will be modified by the addition of the pre-head SKIP instructions, and by the rewriting of conditional latch instructions into conditional exit jump + unconditional backjump.

Definition at line 15 of file dfcc_check_loop_normal_form.cpp.