cprover
|
A base class for assigns clause targets. More...
#include <code_contracts.h>
Public Types | |
enum | target_type { Scalar, Struct, Array } |
Public Member Functions | |
assigns_clause_targett (target_type type, const exprt object_ptr, const code_contractst &contract, messaget &log_parameter) | |
virtual | ~assigns_clause_targett () |
virtual std::vector< symbol_exprt > | temporary_declarations () const =0 |
virtual exprt | alias_expression (const exprt &lhs)=0 |
virtual exprt | compatible_expression (const assigns_clause_targett &called_target)=0 |
virtual goto_programt | havoc_code (source_locationt location) const =0 |
const exprt & | get_direct_pointer () const |
goto_programt & | get_init_block () |
Static Public Member Functions | |
static exprt | pointer_for (const exprt &exp) |
Public Attributes | |
const target_type | target_type |
Protected Attributes | |
const exprt | pointer_object |
const code_contractst & | contract |
goto_programt | init_block |
messaget & | log |
A base class for assigns clause targets.
Definition at line 205 of file code_contracts.h.
Enumerator | |
---|---|
Scalar | |
Struct | |
Array |
Definition at line 208 of file code_contracts.h.
|
inline |
Definition at line 215 of file code_contracts.h.
|
inlinevirtual |
Definition at line 231 of file code_contracts.h.
Implemented in assigns_clause_array_targett, assigns_clause_struct_targett, and assigns_clause_scalar_targett.
|
pure virtual |
Implemented in assigns_clause_array_targett, assigns_clause_struct_targett, and assigns_clause_scalar_targett.
|
inline |
Definition at line 241 of file code_contracts.h.
|
inline |
Definition at line 246 of file code_contracts.h.
|
pure virtual |
Implemented in assigns_clause_array_targett, assigns_clause_struct_targett, and assigns_clause_scalar_targett.
Definition at line 251 of file code_contracts.h.
|
pure virtual |
Implemented in assigns_clause_array_targett, assigns_clause_struct_targett, and assigns_clause_scalar_targett.
|
protected |
Definition at line 260 of file code_contracts.h.
|
protected |
Definition at line 261 of file code_contracts.h.
|
protected |
Definition at line 262 of file code_contracts.h.
|
protected |
Definition at line 259 of file code_contracts.h.
Definition at line 256 of file code_contracts.h.