cprover
code_contractst Member List

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

add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest)code_contractstprotected
add_pointer_checks(const std::string &)code_contractstprotected
apply_contract(goto_programt &goto_program, goto_programt::targett target)code_contractstprotected
check_for_looped_mallocs(const goto_programt &)code_contractstprotected
code_contracts(goto_functionst::goto_functiont &goto_function)code_contractstprotected
code_contractst(goto_modelt &goto_model, messaget &log)code_contractstinline
enforce_contract(const std::string &)code_contractstprotected
enforce_contracts(const std::set< std::string > &)code_contractst
enforce_contracts()code_contractst
goto_functionscode_contractstprotected
has_contract(const irep_idt)code_contractstprotected
instrument_assigns_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::vector< exprt > &original_references, std::set< exprt > &freely_assignable_exprs)code_contractstprotected
instrument_call_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::vector< exprt > &assigns_references, std::set< exprt > &freely_assignable_exprs)code_contractstprotected
logcode_contractstprotected
new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode)code_contractstprotected
nscode_contractstprotected
populate_assigns_references(const symbolt &f_sym, const irep_idt &func_id, goto_programt &created_decls, std::vector< exprt > &created_references)code_contractstprotected
replace_calls(const std::set< std::string > &)code_contractst
replace_calls()code_contractst
summarizedcode_contractstprotected
symbol_tablecode_contractstprotected
temporary_countercode_contractstprotected