#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:

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`. More...

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;

@ GOTO

Definition: goto_program.h:34

OR

The loop has two or more instructions and:

has a unique head instruction;
has a unique, unconditional GOTO latch instruction;
has a pre-head SKIP instruction that is not part of the loop;
the head has two incoming edges from the pre-head and the latch;
for all instructions but the head, incoming edges are from instructions in the same loop;
all instructions of the loop are found between the head and the latch in the instruction sequence;
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.