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 &wrapper_function, const irep_idt &mangled_function, goto_programt &dest)code_contractstprotected
add_quantified_variable(const exprt &expression, replace_symbolt &replace, const irep_idt &mode)code_contractstprotected
apply_function_contract(goto_programt &goto_program, goto_programt::targett target)code_contractstprotected
apply_loop_contract(const irep_idt &function, goto_functionst::goto_functiont &goto_function)code_contractstprotected
apply_loop_contracts()code_contractst
check_apply_loop_contracts(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_contractstprotected
check_frame_conditions(goto_programt &program, const symbolt &target)code_contractstprotected
check_frame_conditions_function(const irep_idt &function)code_contractstprotected
code_contractst(goto_modelt &goto_model, messaget &log)code_contractstinline
convertercode_contractstprotected
create_alias_expression(const exprt &lhs, std::vector< exprt > &aliasable_references)code_contractstprotected
create_ensures_instruction(codet &expression, source_locationt location, const irep_idt &mode)code_contractstprotected
enforce_contract(const irep_idt &function)code_contractstprotected
enforce_contracts(const std::set< std::string > &functions)code_contractst
enforce_contracts()code_contractst
get_goto_functions()code_contractst
get_symbol_table()code_contractst
goto_functionscode_contractstprotected
has_contract(const irep_idt)code_contractstprotected
instrument_assign_statement(goto_programt::instructionst::iterator &instruction_it, goto_programt &program, exprt &assigns, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause)code_contractstprotected
instrument_call_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause)code_contractstprotected
logcode_contractstprotected
new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &mode)code_contractst
nscode_contractst
replace_calls(const std::set< std::string > &functions)code_contractst
replace_calls()code_contractst
replace_history_parameter(exprt &expr, std::map< exprt, exprt > &parameter2history, source_locationt location, const irep_idt &mode, goto_programt &history, const irep_idt &id)code_contractstprotected
summarizedcode_contractstprotected
symbol_tablecode_contractstprotected