#include <dfcc_swap_and_wrap.h>
|
| 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. More...
|
|
|
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 . More...
|
|
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 . More...
|
|
Definition at line 41 of file dfcc_swap_and_wrap.h.
◆ dfcc_swap_and_wrapt()
◆ check_contract()
void dfcc_swap_and_wrapt::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 |
|
) |
| |
|
protected |
Swaps-and-wraps the given function_id
in a wrapper function that checks the given contract_id
.
Generates globals statics:
static bool __contract_check_in_progress = false;
static bool __contract_checked_once = false;
Adds the following instructions in the wrapper function body:
ASSERT !__contract_checked_once
"only a single top-level called allowed";
__contract_check_in_progress = true;
__contract_checked_once = true;
__contract_check_in_progress = false;
ASSERT false,
"no recursive calls";
end:
dfcc_contract_handlert & contract_handler
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition at line 153 of file dfcc_swap_and_wrap.cpp.
◆ get_swapped_functions()
void dfcc_swap_and_wrapt::get_swapped_functions |
( |
std::set< irep_idt > & |
dest | ) |
const |
◆ replace_with_contract()
void dfcc_swap_and_wrapt::replace_with_contract |
( |
const irep_idt & |
function_id, |
|
|
const irep_idt & |
contract_id, |
|
|
std::set< irep_idt > & |
function_pointer_contracts |
|
) |
| |
|
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.
◆ swap_and_wrap()
◆ swap_and_wrap_check()
void dfcc_swap_and_wrapt::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 |
|
) |
| |
|
inline |
◆ swap_and_wrap_replace()
void dfcc_swap_and_wrapt::swap_and_wrap_replace |
( |
const irep_idt & |
function_id, |
|
|
const irep_idt & |
contract_id, |
|
|
std::set< irep_idt > & |
function_pointer_contracts |
|
) |
| |
|
inline |
◆ cache
remember all functions that were swapped/wrapped and in which mode
Definition at line 99 of file dfcc_swap_and_wrap.h.
◆ contract_handler
◆ goto_model
◆ instrument
◆ library
◆ log
◆ message_handler
◆ ns
◆ spec_functions
The documentation for this class was generated from the following files: