cprover
|
#include <dfcc_swap_and_wrap.h>
Public Member Functions | |
dfcc_swap_and_wrapt (goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_spec_functionst &spec_functions, dfcc_contract_handlert &contract_handler) | |
void | swap_and_wrap_check (const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls) |
void | swap_and_wrap_replace (const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts) |
void | get_swapped_functions (std::set< irep_idt > &dest) const |
Adds the set of swapped functions to dest. | |
Protected Member Functions | |
void | swap_and_wrap (const dfcc_contract_modet contract_mode, const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls) |
void | check_contract (const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls) |
Swaps-and-wraps the given function_id in a wrapper function that checks the given contract_id . | |
void | replace_with_contract (const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts) |
Swaps-and-wraps the given function_id in a wrapper function that models the abstract behaviour of contract contract_id . | |
Static Protected Attributes | |
static std::map< irep_idt, std::pair< irep_idt, std::pair< dfcc_contract_modet, loop_contract_configt > > > | cache |
remember all functions that were swapped/wrapped and in which mode | |
Definition at line 41 of file dfcc_swap_and_wrap.h.
dfcc_swap_and_wrapt::dfcc_swap_and_wrapt | ( | goto_modelt & | goto_model, |
message_handlert & | message_handler, | ||
dfcc_libraryt & | library, | ||
dfcc_instrumentt & | instrument, | ||
dfcc_spec_functionst & | spec_functions, | ||
dfcc_contract_handlert & | contract_handler ) |
Definition at line 37 of file dfcc_swap_and_wrap.cpp.
|
protected |
Swaps-and-wraps the given function_id
in a wrapper function that checks the given contract_id
.
Generates globals statics:
Adds the following instructions in the wrapper function body:
Definition at line 153 of file dfcc_swap_and_wrap.cpp.
void dfcc_swap_and_wrapt::get_swapped_functions | ( | std::set< irep_idt > & | dest | ) | const |
Adds the set of swapped functions to dest.
Definition at line 121 of file dfcc_swap_and_wrap.cpp.
|
protected |
Swaps-and-wraps the given function_id
in a wrapper function that models the abstract behaviour of contract contract_id
.
Definition at line 285 of file dfcc_swap_and_wrap.cpp.
|
protected |
Definition at line 61 of file dfcc_swap_and_wrap.cpp.
|
inline |
Definition at line 52 of file dfcc_swap_and_wrap.h.
|
inline |
Definition at line 68 of file dfcc_swap_and_wrap.h.
|
staticprotected |
remember all functions that were swapped/wrapped and in which mode
Definition at line 99 of file dfcc_swap_and_wrap.h.
|
protected |
Definition at line 92 of file dfcc_swap_and_wrap.h.
|
protected |
Definition at line 86 of file dfcc_swap_and_wrap.h.
|
protected |
Definition at line 90 of file dfcc_swap_and_wrap.h.
|
protected |
Definition at line 89 of file dfcc_swap_and_wrap.h.
|
protected |
Definition at line 88 of file dfcc_swap_and_wrap.h.
|
protected |
Definition at line 87 of file dfcc_swap_and_wrap.h.
|
protected |
Definition at line 93 of file dfcc_swap_and_wrap.h.
|
protected |
Definition at line 91 of file dfcc_swap_and_wrap.h.