16 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SWAP_AND_WRAP_H
17 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SWAP_AND_WRAP_H
56 std::set<irep_idt> &function_pointer_contracts,
57 bool allow_recursive_calls)
64 function_pointer_contracts,
65 allow_recursive_calls);
71 std::set<irep_idt> &function_pointer_contracts)
78 function_pointer_contracts,
98 std::pair<irep_idt, std::pair<dfcc_contract_modet, loop_contract_configt>>>
106 std::set<irep_idt> &function_pointer_contracts,
107 bool allow_recursive_calls);
115 std::set<irep_idt> &function_pointer_contracts,
116 bool allow_recursive_calls);
123 std::set<irep_idt> &function_pointer_contracts);
A class for an expression that represents a conditional target or a list of targets sharing a common ...
A contract is represented by a function declaration or definition with contract clauses attached to i...
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
Class interface to library types and functions defined in cprover_contracts.c.
This class rewrites GOTO functions that use the built-ins:
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.
message_handlert & message_handler
dfcc_spec_functionst & spec_functions
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)
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_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.
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
dfcc_instrumentt & instrument
dfcc_contract_handlert & contract_handler
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 con...
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)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Specialisation of dfcc_contract_handlert for contracts.
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.
Add instrumentation to a goto program to perform frame condition checks.
Dynamic frame condition checking library loading.
Translate functions that specify assignable and freeable targets declaratively into active functions ...
Goto Programs with Functions.
API to expression classes.
Loop contract configurations.