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.
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.
void instrument_preconditions | ( | const goto_modelt & | goto_model, |
goto_programt & | goto_program | ||
) |
Definition at line 90 of file instrument_preconditions.cpp.
void instrument_preconditions | ( | goto_modelt & | goto_model | ) |
Definition at line 131 of file instrument_preconditions.cpp.
void remove_preconditions | ( | goto_functiont & | goto_function | ) |
Definition at line 144 of file instrument_preconditions.cpp.
void remove_preconditions | ( | goto_modelt & | goto_model | ) |
Definition at line 149 of file instrument_preconditions.cpp.
void remove_preconditions | ( | goto_programt & | goto_program | ) |
Definition at line 48 of file instrument_preconditions.cpp.