dfcc_check_loop_normal_form.cpp File Reference

#include "dfcc_check_loop_normal_form.h"
#include <analyses/natural_loops.h>
#include <goto-instrument/contracts/utils.h>

Include dependency graph for dfcc_check_loop_normal_form.cpp:

Go to the source code of this file.

Functions
void	dfcc_check_loop_normal_form (goto_programt &goto_program, messaget &log)
	Checks and enforces normal form properties for natural loops of the given goto_program.

Function Documentation

dfcc_check_loop_normal_form()

void dfcc_check_loop_normal_form	(	goto_programt &	goto_program,
		messaget &	log
	)

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:

START: IF expr GOTO START;

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.