CBMC
|
Checks normal form properties of natural loops in a GOTO program. More...
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 . More... | |
Checks normal form properties of natural loops in a GOTO program.
Definition in file dfcc_check_loop_normal_form.h.
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:
OR
The loop has two or more instructions and:
Definition at line 15 of file dfcc_check_loop_normal_form.cpp.