CBMC
dfcc_instrument_loopt Member List

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

add_body_instructions(const std::size_t loop_id, const std::size_t cbmc_loop_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, exprt &invariant, const exprt::operandst &decreases_clauses, const symbol_exprt &entered_loop, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars, const std::vector< symbol_exprt > &new_decreases_vars, const goto_programt::instructiont::targett &step_case_target, const irep_idt &symbol_mode)dfcc_instrument_looptprotected
add_exit_instructions(const std::size_t loop_id, const std::size_t cbmc_loop_id, goto_functionst::goto_functiont &goto_function, goto_programt::targett loop_head, const symbol_exprt &loop_write_set, const symbol_exprt &addr_of_loop_write_set, const std::unordered_map< exprt, symbol_exprt, irep_hash > &history_var_map, const symbol_exprt &entered_loop, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars, const std::vector< symbol_exprt > &new_decreases_vars)dfcc_instrument_looptprotected
add_prehead_instructions(const std::size_t loop_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &assigns_instrs, exprt &invariant, const exprt::operandst &assigns, const symbol_exprt &loop_write_set, const symbol_exprt &addr_of_loop_write_set, const symbol_exprt &entered_loop, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const irep_idt &symbol_mode)dfcc_instrument_looptprotected
add_step_instructions(const std::size_t loop_id, const std::size_t cbmc_loop_id, const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &havoc_instrs, exprt &invariant, const exprt::operandst &decreases_clauses, const symbol_exprt &loop_write_set, const exprt &outer_write_set, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars)dfcc_instrument_looptprotected
contract_clauses_codegendfcc_instrument_looptprotected
dfcc_instrument_loopt(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen)dfcc_instrument_loopt
get_max_assigns_clause_size() constdfcc_instrument_looptinline
goto_modeldfcc_instrument_looptprotected
librarydfcc_instrument_looptprotected
logdfcc_instrument_looptprotected
max_assigns_clause_sizedfcc_instrument_looptprotected
nsdfcc_instrument_looptprotected
operator()(const std::size_t loop_id, const irep_idt &function_id, goto_functiont &goto_function, dfcc_cfg_infot &cfg_info, const std::set< symbol_exprt > &local_statics, std::set< irep_idt > &function_pointer_contracts)dfcc_instrument_loopt
spec_functionsdfcc_instrument_looptprotected