cprover
|
#include <code_contracts.h>
Public Member Functions | |
assigns_clause_scalar_targett (const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id) | |
std::vector< symbol_exprt > | temporary_declarations () const |
exprt | alias_expression (const exprt &lhs) |
exprt | compatible_expression (const assigns_clause_targett &called_target) |
goto_programt | havoc_code (source_locationt location) const |
![]() | |
assigns_clause_targett (target_type type, const exprt object_ptr, const code_contractst &contract, messaget &log_parameter) | |
virtual | ~assigns_clause_targett () |
const exprt & | get_direct_pointer () const |
goto_programt & | get_init_block () |
Protected Attributes | |
symbol_exprt | local_standin_variable |
![]() | |
const exprt | pointer_object |
const code_contractst & | contract |
goto_programt | init_block |
messaget & | log |
Additional Inherited Members | |
![]() | |
enum | target_type { Scalar, Struct, Array } |
![]() | |
static exprt | pointer_for (const exprt &exp) |
![]() | |
const target_type | target_type |
Definition at line 265 of file code_contracts.h.
assigns_clause_scalar_targett::assigns_clause_scalar_targett | ( | const exprt & | object_ptr, |
code_contractst & | contract, | ||
messaget & | log_parameter, | ||
const irep_idt & | function_id | ||
) |
Definition at line 1020 of file code_contracts.cpp.
Implements assigns_clause_targett.
Definition at line 1059 of file code_contracts.cpp.
|
virtual |
Implements assigns_clause_targett.
Definition at line 1064 of file code_contracts.cpp.
|
virtual |
Implements assigns_clause_targett.
Definition at line 1078 of file code_contracts.cpp.
|
virtual |
Implements assigns_clause_targett.
Definition at line 1052 of file code_contracts.cpp.
|
protected |
Definition at line 280 of file code_contracts.h.