CBMC
|
Program Transformation. More...
Go to the source code of this file.
Functions | |
bool | is_skip (const goto_programt &body, goto_programt::const_targett it, bool ignore_labels) |
Determine whether the instruction is semantically equivalent to a skip (no-op). More... | |
void | remove_skip (goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end) |
remove unnecessary skip statements More... | |
void | remove_skip (goto_programt &goto_program) |
remove unnecessary skip statements More... | |
void | remove_skip (goto_functionst &goto_functions) |
remove unnecessary skip statements More... | |
void | remove_skip (goto_modelt &goto_model) |
Program Transformation.
Definition in file remove_skip.cpp.
bool is_skip | ( | const goto_programt & | body, |
goto_programt::const_targett | it, | ||
bool | ignore_labels | ||
) |
Determine whether the instruction is semantically equivalent to a skip (no-op).
This includes a skip, but also if(false) goto ..., goto next; next: ..., and (void)0.
body | goto program containing the instruction |
it | instruction iterator that is tested for being a skip (or equivalent) |
ignore_labels | If the caller takes care of moving labels, then even skip statements carrying labels can be treated as skips (even though they may carry key information such as error labels). |
Definition at line 27 of file remove_skip.cpp.
void remove_skip | ( | goto_functionst & | goto_functions | ) |
remove unnecessary skip statements
Definition at line 199 of file remove_skip.cpp.
void remove_skip | ( | goto_modelt & | goto_model | ) |
Definition at line 213 of file remove_skip.cpp.
void remove_skip | ( | goto_programt & | goto_program | ) |
remove unnecessary skip statements
Definition at line 188 of file remove_skip.cpp.
void remove_skip | ( | goto_programt & | goto_program, |
goto_programt::targett | begin, | ||
goto_programt::targett | end | ||
) |
remove unnecessary skip statements
goto_program | goto program containing the instructions to be cleaned in the range [begin, end) |
begin | iterator pointing to first instruction to be considered |
end | iterator pointing beyond last instruction to be considered |
Definition at line 87 of file remove_skip.cpp.