cprover
|
Public Member Functions | |
code_contractst (symbol_tablet &_symbol_table, goto_functionst &_goto_functions) | |
void | operator() () |
Protected Types | |
typedef std::unordered_set< irep_idt, irep_id_hash > | id_sett |
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 |
id_sett | summarized |
Definition at line 26 of file code_contracts.cpp.
|
protected |
Definition at line 48 of file code_contracts.cpp.
|
inline |
Definition at line 29 of file code_contracts.cpp.
References operator()().
Referenced by code_contracts().
|
protected |
Definition at line 260 of file code_contracts.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), code_function_callt::arguments(), DECL, goto_program_templatet< codeT, guardT >::destructive_append(), goto_program_templatet< codeT, guardT >::destructive_insert(), code_function_callt::function(), goto_functions_templatet< bodyT >::function_map, goto_functions, replace_symbolt::insert(), goto_program_templatet< codeT, guardT >::instructions, irept::is_not_nil(), code_function_callt::lhs(), namespacet::lookup(), new_tmp_symbol(), ns, r, SKIP, 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(), code_function_callt::function(), irept::id(), replace_symbolt::insert(), goto_program_templatet< codeT, guardT >::insert_before_swap(), irept::is_nil(), irept::is_not_nil(), code_function_callt::lhs(), namespacet::lookup(), ns, code_typet::parameters(), code_typet::return_type(), exprt::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(), and symbol_table.
Referenced by add_contract_check().
void code_contractst::operator() | ( | void | ) |
Definition at line 383 of file code_contracts.cpp.
References add_contract_check(), code_contracts(), CPROVER_PREFIX, Forall_goto_functions, goto_functions_templatet< bodyT >::function_map, goto_functions, remove_skip(), summarized, and goto_functions_templatet< bodyT >::update().
Referenced by code_contractst().
|
protected |
Definition at line 44 of file code_contracts.cpp.
Referenced by add_contract_check(), and operator()().
|
protected |
Definition at line 42 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 43 of file code_contracts.cpp.
Referenced by new_tmp_symbol().
|
protected |
Definition at line 46 of file code_contracts.cpp.