dfcc_swap_and_wrapt Class Reference

#include <dfcc_swap_and_wrap.h>

Collaboration diagram for dfcc_swap_and_wrapt:

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 dfcc_loop_contract_modet loop_contract_mode, 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...

Protected Member Functions
void	swap_and_wrap (const dfcc_contract_modet contract_mode, const dfcc_loop_contract_modet loop_contract_mode, 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 dfcc_loop_contract_modet loop_contract_mode, 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...

Protected Attributes
goto_modelt &	goto_model
message_handlert &	message_handler
messaget	log
dfcc_libraryt &	library
dfcc_instrumentt &	instrument
dfcc_spec_functionst &	spec_functions
dfcc_contract_handlert &	contract_handler
namespacet	ns

Static Protected Attributes
static std::map< irep_idt, std::pair< irep_idt, std::pair< dfcc_contract_modet, dfcc_loop_contract_modet > > >	cache
	remember all functions that were swapped/wrapped and in which mode More...

Detailed Description

Definition at line 41 of file dfcc_swap_and_wrap.h.

Constructor & Destructor Documentation

dfcc_swap_and_wrapt()

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.

Member Function Documentation

check_contract()

void dfcc_swap_and_wrapt::check_contract ( const dfcc_loop_contract_modet  loop_contract_mode, 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:

IF __contract_check_in_progress GOTO replace;
ASSERT !__contract_checked_once "only a single top-level called allowed";
__contract_check_in_progress = true;
<contract_handler.add_contract_checking_instructions(...)>;
__contract_checked_once = true;
__contract_check_in_progress = false;
GOTO end;
replace:
// if allow_recursive_calls
<contract_handler.add_contract_replacement_instructions(...)>;
// if !allow_recursive_calls
ASSERT false, "no recursive calls";
ASSUME false;
end:
END_FUNCTION;

Definition at line 154 of file dfcc_swap_and_wrap.cpp.

get_swapped_functions()

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 122 of file dfcc_swap_and_wrap.cpp.

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 286 of file dfcc_swap_and_wrap.cpp.

swap_and_wrap()

void dfcc_swap_and_wrapt::swap_and_wrap ( const dfcc_contract_modet  contract_mode, const dfcc_loop_contract_modet  loop_contract_mode, const irep_idt &  function_id, const irep_idt &  contract_id, std::set< irep_idt > &  function_pointer_contracts, bool  allow_recursive_calls  )

protected

Definition at line 61 of file dfcc_swap_and_wrap.cpp.

swap_and_wrap_check()

void dfcc_swap_and_wrapt::swap_and_wrap_check ( const dfcc_loop_contract_modet  loop_contract_mode, const irep_idt &  function_id, const irep_idt &  contract_id, std::set< irep_idt > &  function_pointer_contracts, bool  allow_recursive_calls  )

inline

Definition at line 52 of file dfcc_swap_and_wrap.h.

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

Definition at line 68 of file dfcc_swap_and_wrap.h.

Member Data Documentation

cache

std::map< irep_idt, std::pair< irep_idt, std::pair< dfcc_contract_modet, dfcc_loop_contract_modet > > > dfcc_swap_and_wrapt::cache

staticprotected

remember all functions that were swapped/wrapped and in which mode

Definition at line 100 of file dfcc_swap_and_wrap.h.

contract_handler

dfcc_contract_handlert& dfcc_swap_and_wrapt::contract_handler

protected

Definition at line 92 of file dfcc_swap_and_wrap.h.

goto_model

goto_modelt& dfcc_swap_and_wrapt::goto_model

protected

Definition at line 86 of file dfcc_swap_and_wrap.h.

instrument

dfcc_instrumentt& dfcc_swap_and_wrapt::instrument

protected

Definition at line 90 of file dfcc_swap_and_wrap.h.

library

dfcc_libraryt& dfcc_swap_and_wrapt::library

protected

Definition at line 89 of file dfcc_swap_and_wrap.h.

log

messaget dfcc_swap_and_wrapt::log

protected

Definition at line 88 of file dfcc_swap_and_wrap.h.

message_handler

message_handlert& dfcc_swap_and_wrapt::message_handler

protected

Definition at line 87 of file dfcc_swap_and_wrap.h.

ns

namespacet dfcc_swap_and_wrapt::ns

protected

Definition at line 93 of file dfcc_swap_and_wrap.h.

spec_functions

dfcc_spec_functionst& dfcc_swap_and_wrapt::spec_functions

protected

Definition at line 91 of file dfcc_swap_and_wrap.h.

---

The documentation for this class was generated from the following files:

• /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h
• /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp