cprover
|
A base class for assigns clause targets. More...
#include <assigns.h>
Public Member Functions | |
assigns_clause_targett (const exprt &object, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id) | |
~assigns_clause_targett () | |
std::vector< symbol_exprt > | temporary_declarations () const |
exprt | alias_expression (const exprt &lhs) |
exprt | compatible_expression (const assigns_clause_targett &called_target) |
const exprt & | get_direct_pointer () const |
goto_programt & | get_init_block () |
Static Public Member Functions | |
static exprt | pointer_for (const exprt &object) |
Protected Attributes | |
const exprt | pointer_object |
const code_contractst & | contract |
goto_programt | init_block |
messaget & | log |
symbol_exprt | target |
const irep_idt & | target_id |
assigns_clause_targett::assigns_clause_targett | ( | const exprt & | object, |
code_contractst & | contract, | ||
messaget & | log_parameter, | ||
const irep_idt & | function_id | ||
) |
Definition at line 22 of file assigns.cpp.
assigns_clause_targett::~assigns_clause_targett | ( | ) |
Definition at line 53 of file assigns.cpp.
Definition at line 64 of file assigns.cpp.
exprt assigns_clause_targett::compatible_expression | ( | const assigns_clause_targett & | called_target | ) |
Definition at line 103 of file assigns.cpp.
const exprt & assigns_clause_targett::get_direct_pointer | ( | ) | const |
Definition at line 109 of file assigns.cpp.
goto_programt & assigns_clause_targett::get_init_block | ( | ) |
Definition at line 114 of file assigns.cpp.
std::vector< symbol_exprt > assigns_clause_targett::temporary_declarations | ( | ) | const |
Definition at line 57 of file assigns.cpp.
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |