CBMC
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 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...
 

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. 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_modeltgoto_model
 
message_handlertmessage_handler
 
messaget log
 
dfcc_librarytlibrary
 
dfcc_instrumenttinstrument
 
dfcc_spec_functionstspec_functions
 
dfcc_contract_handlertcontract_handler
 
namespacet ns
 

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 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 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:

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;
// if allow_recursive_calls
<contract_handler.add_contract_replacement_instructions(...)>;
// if !allow_recursive_calls
ASSERT false, "no recursive calls";
ASSUME false;
end:
dfcc_contract_handlert & contract_handler
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSERT
Definition: goto_program.h:36
@ GOTO
Definition: goto_program.h:34
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

Adds the set of swapped functions to dest.

Definition at line 121 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 285 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 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

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 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

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, loop_contract_configt > > > dfcc_swap_and_wrapt::cache
staticprotected

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

Definition at line 99 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: