cprover
|
This is the complete list of members for code_contractst, including all inherited members.
add_contract_check(const irep_idt &wrapper_function, const irep_idt &mangled_function, goto_programt &dest) | code_contractst | protected |
add_quantified_variable(const exprt &expression, replace_symbolt &replace, const irep_idt &mode) | code_contractst | protected |
apply_function_contract(const irep_idt &function, const source_locationt &location, goto_programt &function_body, goto_programt::targett &target) | code_contractst | protected |
apply_loop_contract(const irep_idt &function, goto_functionst::goto_functiont &goto_function) | code_contractst | protected |
apply_loop_contracts() | code_contractst | |
check_apply_loop_contracts(const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, const loopt &loop, const irep_idt &mode) | code_contractst | |
check_for_looped_mallocs(const goto_programt &program) | code_contractst | protected |
check_frame_conditions(const irep_idt &function, goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, instrument_spec_assignst &instrument_spec_assigns, skipt skip_parameter_assigns, optionalt< cfg_infot > &cfg_info_opt) | code_contractst | protected |
check_frame_conditions_function(const irep_idt &function) | code_contractst | protected |
code_contractst(goto_modelt &goto_model, messaget &log) | code_contractst | inline |
converter | code_contractst | protected |
create_ensures_instruction(codet &expression, source_locationt location, const irep_idt &mode) | code_contractst | protected |
enforce_contract(const irep_idt &function) | code_contractst | protected |
enforce_contracts(const std::set< std::string > &functions) | code_contractst | |
get_goto_functions() | code_contractst | |
get_symbol_table() | code_contractst | |
goto_functions | code_contractst | protected |
instrument_assign_statement(goto_programt::targett &instruction_it, goto_programt &program, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt) | code_contractst | protected |
instrument_call_statement(goto_programt::targett &instruction_it, const irep_idt &function, goto_programt &body, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt) | code_contractst | protected |
log | code_contractst | protected |
ns | code_contractst | |
replace_calls(const std::set< std::string > &) | code_contractst | |
replace_history_parameter(exprt &expr, std::map< exprt, exprt > ¶meter2history, source_locationt location, const irep_idt &mode, goto_programt &history, const irep_idt &id) | code_contractst | protected |
skipt enum name | code_contractst | |
summarized | code_contractst | protected |
symbol_table | code_contractst | protected |