cprover
|
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_contractst | protected |
add_pointer_checks(const std::string &) | code_contractst | protected |
add_quantified_variable(exprt expression, replace_symbolt &replace, irep_idt mode) | code_contractst | protected |
apply_function_contract(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target) | code_contractst | protected |
apply_loop_contract(goto_functionst::goto_functiont &goto_function) | code_contractst | protected |
check_for_looped_mallocs(const goto_programt &) | code_contractst | protected |
code_contractst(goto_modelt &goto_model, messaget &log) | code_contractst | inline |
convert_to_goto(const codet &code, const irep_idt &mode, goto_programt &program) | code_contractst | protected |
create_alias_expression(const exprt &lhs, std::vector< exprt > &aliasable_references) | code_contractst | protected |
enforce_contract(const std::string &) | code_contractst | protected |
enforce_contracts(const std::set< std::string > &) | code_contractst | |
enforce_contracts() | code_contractst | |
goto_functions | code_contractst | protected |
has_contract(const irep_idt) | code_contractst | protected |
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_contractst | protected |
instrument_call_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, const irep_idt &function_id, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause) | code_contractst | protected |
log | code_contractst | protected |
new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode) | code_contractst | |
ns | code_contractst | |
populate_assigns_reference(std::vector< exprt > operands, const symbolt &function_symbol, const irep_idt &function_id, goto_programt &created_declarations, std::vector< exprt > &created_references) | code_contractst | protected |
replace_calls(const std::set< std::string > &) | code_contractst | |
replace_calls() | code_contractst | |
summarized | code_contractst | protected |
symbol_table | code_contractst | protected |
temporary_counter | code_contractst | protected |