CBMC
|
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_instrumentt | protected |
contract_clauses_codegen | dfcc_instrumentt | protected |
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) const | dfcc_instrumentt | |
function_cache | dfcc_instrumentt | protectedstatic |
get_instrumented_functions(std::set< irep_idt > &dest) const | dfcc_instrumentt | |
get_local_statics(const irep_idt &function_id) | dfcc_instrumentt | protected |
get_max_assigns_clause_size() const | dfcc_instrumentt | |
goto_model | dfcc_instrumentt | protected |
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_instrumentt | protected |
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_instrumentt | protected |
instrument_assign(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info) | dfcc_instrumentt | protected |
instrument_call_instruction(const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program) | dfcc_instrumentt | protected |
instrument_dead(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info) | dfcc_instrumentt | protected |
instrument_deallocate_call(const irep_idt &function_id, const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program) | dfcc_instrumentt | protected |
instrument_decl(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info) | dfcc_instrumentt | protected |
instrument_fptr_call_instruction_dynamic_lookup(const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program) | dfcc_instrumentt | protected |
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_instrumentt | protected |
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_instrumentt | protected |
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_instrumentt | protected |
instrument_lhs(const irep_idt &function_id, goto_programt::targett &target, const exprt &lhs, goto_programt &goto_program, dfcc_cfg_infot &cfg_info) | dfcc_instrumentt | protected |
instrument_loop | dfcc_instrumentt | protected |
instrument_other(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info) | dfcc_instrumentt | protected |
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_symbols | dfcc_instrumentt | protected |
is_dead_object_update(const exprt &lhs, const exprt &rhs) | dfcc_instrumentt | protected |
is_internal_symbol(const irep_idt &id) const | dfcc_instrumentt | |
library | dfcc_instrumentt | protected |
log | dfcc_instrumentt | protected |
message_handler | dfcc_instrumentt | protected |
ns | dfcc_instrumentt | protected |
spec_functions | dfcc_instrumentt | protected |