cprover
|
Go to the source code of this file.
Functions | |
std::vector< goto_programt::const_targett > | get_preconditions (const symbol_exprt &function, const goto_functionst &goto_functions) |
void | remove_preconditions (goto_programt &goto_program) |
replace_symbolt | actuals_replace_map (const code_function_callt &call, const namespacet &ns) |
void | instrument_preconditions (const goto_modelt &goto_model, goto_programt &goto_program) |
void | instrument_preconditions (goto_modelt &goto_model) |
void | remove_preconditions (goto_functiont &goto_function) |
void | remove_preconditions (goto_modelt &goto_model) |
replace_symbolt actuals_replace_map | ( | const code_function_callt & | call, |
const namespacet & | ns | ||
) |
Definition at line 64 of file instrument_preconditions.cpp.
References code_function_callt::arguments(), code_function_callt::function(), irept::id(), replace_symbolt::insert(), namespacet::lookup(), PRECONDITION, dstringt::size(), to_code_type(), to_symbol_expr(), and exprt::type().
Referenced by instrument_preconditions().
std::vector<goto_programt::const_targett> get_preconditions | ( | const symbol_exprt & | function, |
const goto_functionst & | goto_functions | ||
) |
Definition at line 16 of file instrument_preconditions.cpp.
References goto_functionst::function_map.
Referenced by instrument_preconditions().
void instrument_preconditions | ( | const goto_modelt & | goto_model, |
goto_programt & | goto_program | ||
) |
Definition at line 93 of file instrument_preconditions.cpp.
References actuals_replace_map(), get_preconditions(), goto_modelt::goto_functions, goto_program, goto_programt::insert_before_swap(), goto_programt::instructions, r, source_locationt::set_property_class(), goto_modelt::symbol_table, to_code_function_call(), and to_symbol_expr().
Referenced by instrument_preconditions(), jbmc_parse_optionst::process_goto_functions(), goto_diff_parse_optionst::process_goto_program(), jdiff_parse_optionst::process_goto_program(), and cbmc_parse_optionst::process_goto_program().
void instrument_preconditions | ( | goto_modelt & | goto_model | ) |
Definition at line 137 of file instrument_preconditions.cpp.
References goto_functionst::function_map, goto_modelt::goto_functions, instrument_preconditions(), and remove_preconditions().
void remove_preconditions | ( | goto_programt & | goto_program | ) |
Definition at line 48 of file instrument_preconditions.cpp.
References goto_program, goto_programt::instructions, and LOCATION.
Referenced by instrument_preconditions(), and remove_preconditions().
void remove_preconditions | ( | goto_functiont & | goto_function | ) |
Definition at line 150 of file instrument_preconditions.cpp.
References goto_functiont::body, and remove_preconditions().
void remove_preconditions | ( | goto_modelt & | goto_model | ) |
Definition at line 155 of file instrument_preconditions.cpp.
References goto_functionst::function_map, goto_modelt::goto_functions, and remove_preconditions().