dfcc_wrapper_programt Member List

This is the complete list of members for dfcc_wrapper_programt, including all inherited members.

add_to_dest(goto_programt &dest, std::set< irep_idt > &dest_fp_contracts)	dfcc_wrapper_programt
add_to_dest(goto_programt &dest)	dfcc_wrapper_programt	protected
addr_of_contract_write_set	dfcc_wrapper_programt	protected
addr_of_ensures_write_set	dfcc_wrapper_programt	protected
addr_of_is_fresh_set	dfcc_wrapper_programt	protected
addr_of_requires_write_set	dfcc_wrapper_programt	protected
caller_write_set	dfcc_wrapper_programt	protected
contract_code_type	dfcc_wrapper_programt	protected
contract_functions	dfcc_wrapper_programt	protected
contract_lambda_parameters	dfcc_wrapper_programt	protected
contract_mode	dfcc_wrapper_programt	protected
contract_symbol	dfcc_wrapper_programt	protected
contract_write_set	dfcc_wrapper_programt	protected
converter	dfcc_wrapper_programt	protected
dfcc_wrapper_programt(const dfcc_contract_modet contract_mode, const symbolt &wrapper_symbol, const symbolt &wrapped_symbol, const dfcc_contract_functionst &contract_functions, const symbolt &caller_write_set_symbol, goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates)	dfcc_wrapper_programt
encode_checked_function_call()	dfcc_wrapper_programt	protected
encode_contract_write_set()	dfcc_wrapper_programt	protected
encode_ensures_clauses()	dfcc_wrapper_programt	protected
encode_ensures_write_set()	dfcc_wrapper_programt	protected
encode_function_call()	dfcc_wrapper_programt	protected
encode_havoced_function_call()	dfcc_wrapper_programt	protected
encode_is_fresh_set()	dfcc_wrapper_programt	protected
encode_requires_clauses()	dfcc_wrapper_programt	protected
encode_requires_write_set()	dfcc_wrapper_programt	protected
ensures_write_set	dfcc_wrapper_programt	protected
function_call	dfcc_wrapper_programt	protected
function_pointer_contracts	dfcc_wrapper_programt	protected
goto_model	dfcc_wrapper_programt	protected
history	dfcc_wrapper_programt	protected
instrument	dfcc_wrapper_programt	protected
is_fresh_set	dfcc_wrapper_programt	protected
library	dfcc_wrapper_programt	protected
link_allocated_caller	dfcc_wrapper_programt	protected
link_deallocated_contract	dfcc_wrapper_programt	protected
link_is_fresh	dfcc_wrapper_programt	protected
log	dfcc_wrapper_programt	protected
memory_predicates	dfcc_wrapper_programt	protected
message_handler	dfcc_wrapper_programt	protected
ns	dfcc_wrapper_programt	protected
postamble	dfcc_wrapper_programt	protected
postconditions	dfcc_wrapper_programt	protected
preamble	dfcc_wrapper_programt	protected
preconditions	dfcc_wrapper_programt	protected
requires_write_set	dfcc_wrapper_programt	protected
return_value_opt	dfcc_wrapper_programt	protected
wrapped_symbol	dfcc_wrapper_programt	protected
wrapper_sl	dfcc_wrapper_programt	protected
wrapper_symbol	dfcc_wrapper_programt	protected
write_set_checks	dfcc_wrapper_programt	protected