cprover
Loading...
Searching...
No Matches
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.

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.

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

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:

Adds the following instructions in the wrapper function body:

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: