CBMC
dfcc_instrumentt Member List

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

apply_loop_contracts(const irep_idt &function_id, goto_functiont &goto_function, dfcc_cfg_infot &cfg_info, const loop_contract_configt &loop_contract_config, const std::set< symbol_exprt > &local_statics, std::set< irep_idt > &function_pointer_contracts)dfcc_instrumenttprotected
contract_clauses_codegendfcc_instrumenttprotected
dfcc_instrumentt(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen)dfcc_instrumentt
do_not_instrument(const irep_idt &id) constdfcc_instrumentt
function_cachedfcc_instrumenttprotectedstatic
get_instrumented_functions(std::set< irep_idt > &dest) constdfcc_instrumentt
get_local_statics(const irep_idt &function_id)dfcc_instrumenttprotected
get_max_assigns_clause_size() constdfcc_instrumentt
goto_modeldfcc_instrumenttprotected
insert_add_decl_call(const irep_idt &function_id, const exprt &write_set, const symbol_exprt &symbol_expr, goto_programt::targett &target, goto_programt &goto_program)dfcc_instrumenttprotected
insert_record_dead_call(const irep_idt &function_id, const exprt &write_set, const symbol_exprt &symbol_expr, goto_programt::targett &target, goto_programt &goto_program)dfcc_instrumenttprotected
instrument_assign(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)dfcc_instrumenttprotected
instrument_call_instruction(const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)dfcc_instrumenttprotected
instrument_dead(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)dfcc_instrumenttprotected
instrument_deallocate_call(const irep_idt &function_id, const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)dfcc_instrumenttprotected
instrument_decl(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)dfcc_instrumenttprotected
instrument_fptr_call_instruction_dynamic_lookup(const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)dfcc_instrumenttprotected
instrument_function(const irep_idt &function_id, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)dfcc_instrumentt
instrument_function_call(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)dfcc_instrumenttprotected
instrument_goto_function(const irep_idt &function_id, goto_functiont &goto_function, const exprt &write_set, const std::set< symbol_exprt > &local_statics, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)dfcc_instrumenttprotected
instrument_goto_program(const irep_idt &function_id, goto_programt &goto_program, const exprt &write_set, std::set< irep_idt > &function_pointer_contracts)dfcc_instrumentt
instrument_harness_function(const irep_idt &function_id, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)dfcc_instrumentt
instrument_instructions(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, dfcc_cfg_infot &cfg_info, std::set< irep_idt > &function_pointer_contracts)dfcc_instrumenttprotected
instrument_lhs(const irep_idt &function_id, goto_programt::targett &target, const exprt &lhs, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)dfcc_instrumenttprotected
instrument_loopdfcc_instrumenttprotected
instrument_other(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)dfcc_instrumenttprotected
instrument_wrapped_function(const irep_idt &wrapped_function_id, const irep_idt &initial_function_id, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)dfcc_instrumentt
internal_symbolsdfcc_instrumenttprotected
is_dead_object_update(const exprt &lhs, const exprt &rhs)dfcc_instrumenttprotected
is_internal_symbol(const irep_idt &id) constdfcc_instrumentt
librarydfcc_instrumenttprotected
logdfcc_instrumenttprotected
message_handlerdfcc_instrumenttprotected
nsdfcc_instrumenttprotected
spec_functionsdfcc_instrumenttprotected