cprover
|
Public Member Functions | |
code_contractst (symbol_tablet &_symbol_table, goto_functionst &_goto_functions) | |
void | operator() () |
Protected Member Functions | |
void | code_contracts (goto_functionst::goto_functiont &goto_function) |
void | apply_contract (goto_programt &goto_program, goto_programt::targett target) |
void | add_contract_check (const irep_idt &function, goto_programt &dest) |
const symbolt & | new_tmp_symbol (const typet &type, const source_locationt &source_location) |
Protected Attributes | |
namespacet | ns |
symbol_tablet & | symbol_table |
goto_functionst & | goto_functions |
unsigned | temporary_counter |
std::unordered_set< irep_idt > | summarized |
Definition at line 27 of file code_contracts.cpp.
|
inline |
Definition at line 30 of file code_contracts.cpp.
|
protected |
Definition at line 260 of file code_contracts.cpp.
References goto_programt::add_instruction(), code_function_callt::arguments(), DECL, goto_programt::destructive_append(), goto_programt::destructive_insert(), code_function_callt::function(), goto_functionst::function_map, goto_functions, replace_symbolt::insert(), goto_programt::instructions, irept::is_not_nil(), code_function_callt::lhs(), namespacet::lookup(), new_tmp_symbol(), ns, r, SKIP, typet::source_location(), and exprt::source_location().
Referenced by operator()().
|
protected |
Definition at line 164 of file code_contracts.cpp.
References code_function_callt::arguments(), ASSERT, irept::find(), goto_programt::instructiont::function, code_function_callt::function(), goto_program, goto_programt::instructiont::guard, irept::id(), replace_symbolt::insert(), goto_programt::insert_before_swap(), irept::is_nil(), irept::is_not_nil(), code_function_callt::lhs(), namespacet::lookup(), ns, code_typet::parameters(), code_typet::return_type(), goto_programt::instructiont::source_location, summarized, to_code_function_call(), to_code_type(), to_symbol_expr(), and symbolt::type.
Referenced by code_contracts().
|
protected |
Definition at line 224 of file code_contracts.cpp.
References apply_contract(), check_apply_invariants(), Forall_goto_program_instructions, and natural_loops_templatet< P, T >::loop_map.
Referenced by operator()().
|
protected |
Definition at line 247 of file code_contracts.cpp.
References get_fresh_aux_symbol(), source_locationt::get_function(), id2string(), and symbol_table.
Referenced by add_contract_check().
void code_contractst::operator() | ( | void | ) |
Definition at line 384 of file code_contracts.cpp.
References add_contract_check(), code_contracts(), Forall_goto_functions, goto_functionst::function_map, goto_functions, INITIALIZE_FUNCTION, remove_skip(), summarized, and goto_functionst::update().
|
protected |
Definition at line 45 of file code_contracts.cpp.
Referenced by add_contract_check(), and operator()().
|
protected |
Definition at line 43 of file code_contracts.cpp.
Referenced by add_contract_check(), and apply_contract().
|
protected |
Definition at line 49 of file code_contracts.cpp.
Referenced by apply_contract(), and operator()().
|
protected |
Definition at line 44 of file code_contracts.cpp.
Referenced by new_tmp_symbol().
|
protected |
Definition at line 47 of file code_contracts.cpp.