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 28 of file code_contracts.cpp.
|
inline |
Definition at line 31 of file code_contracts.cpp.
|
protected |
Definition at line 267 of file code_contracts.cpp.
|
protected |
Definition at line 165 of file code_contracts.cpp.
|
protected |
Definition at line 231 of file code_contracts.cpp.
|
protected |
Definition at line 254 of file code_contracts.cpp.
void code_contractst::operator() | ( | void | ) |
Definition at line 394 of file code_contracts.cpp.
|
protected |
Definition at line 46 of file code_contracts.cpp.
|
protected |
Definition at line 44 of file code_contracts.cpp.
|
protected |
Definition at line 50 of file code_contracts.cpp.
|
protected |
Definition at line 45 of file code_contracts.cpp.
|
protected |
Definition at line 48 of file code_contracts.cpp.