cprover
instrument_preconditions.cpp File Reference
Include dependency graph for instrument_preconditions.cpp:

Go to the source code of this file.

Functions

std::vector< goto_programt::const_targettget_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)
 

Function Documentation

◆ actuals_replace_map()

◆ get_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().

◆ instrument_preconditions() [1/2]

◆ instrument_preconditions() [2/2]

void instrument_preconditions ( goto_modelt goto_model)

◆ remove_preconditions() [1/3]

void remove_preconditions ( goto_programt goto_program)

◆ remove_preconditions() [2/3]

void remove_preconditions ( goto_functiont goto_function)

Definition at line 150 of file instrument_preconditions.cpp.

References goto_functiont::body, and remove_preconditions().

◆ remove_preconditions() [3/3]

void remove_preconditions ( goto_modelt goto_model)