cprover
|
Program Transformation. More...
#include "goto_program.h"
Go to the source code of this file.
Functions | |
bool | is_skip (const goto_programt &, goto_programt::const_targett, bool ignore_labels=false) |
Determine whether the instruction is semantically equivalent to a skip (no-op). More... | |
void | remove_skip (goto_programt &) |
remove unnecessary skip statements More... | |
void | remove_skip (goto_functionst &) |
remove unnecessary skip statements More... | |
void | remove_skip (goto_modelt &) |
void | remove_skip (goto_programt &goto_program, goto_programt::targett begin, const goto_programt::targett end) |
remove unnecessary skip statements More... | |
Program Transformation.
Definition in file remove_skip.h.
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 25 of file remove_skip.cpp.
References code_expressiont::expression(), irept::id(), goto_programt::instructions, exprt::is_constant(), unary_exprt::op(), to_code_expression(), to_typecast_expr(), and exprt::type().
Referenced by goto_convertt::generate_ifthenelse(), is_empty(), and remove_skip().
void remove_skip | ( | goto_programt & | ) |
remove unnecessary skip statements
Definition at line 184 of file remove_skip.cpp.
References goto_program, goto_programt::instructions, remove_skip(), and goto_programt::update().
void remove_skip | ( | goto_functionst & | ) |
remove unnecessary skip statements
Definition at line 195 of file remove_skip.cpp.
References Forall_goto_functions, remove_skip(), and goto_functionst::update().
void remove_skip | ( | goto_modelt & | ) |
Definition at line 207 of file remove_skip.cpp.
References goto_modelt::goto_functions, and remove_skip().
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 86 of file remove_skip.cpp.
References symbol_table_baset::begin(), goto_programt::compute_target_numbers(), symbol_table_baset::end(), goto_program, goto_programt::instructions, and is_skip().
Referenced by sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), scratch_programt::check_sat(), convert_nondet(), string_instrumentationt::do_function_call(), goto_instrument_parse_optionst::doit(), havoc_generate_function_bodiest::generate_function_body_impl(), goto_checkt::goto_check(), havoc_loopst::havoc_loop(), instrument_cover_goals(), remove_exceptionst::instrument_exceptions(), goto_instrument_parse_optionst::instrument_goto_program(), model_argc_argv(), code_contractst::operator()(), full_slicert::operator()(), remove_asmt::process_function(), jbmc_parse_optionst::process_goto_functions(), jdiff_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), k_inductiont::process_loop(), race_check(), remove_function_pointerst::remove_function_pointers(), remove_skip(), remove_virtual_functionst::remove_virtual_function(), replace_java_nondet(), remove_returnst::restore_returns(), reachability_slicert::slice(), slice_global_inits(), static_simplifier(), and weak_memory().