|
CBMC
|
Include dependency graph for remove_skip.cpp: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 196 of file remove_skip.cpp.
| void remove_skip | ( | goto_modelt & | goto_model | ) |
Definition at line 210 of file remove_skip.cpp.
| void remove_skip | ( | goto_programt & | goto_program | ) |
remove unnecessary skip statements
Definition at line 185 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.