cprover
|
#include <code_contracts.h>
Public Member Functions | |
assigns_clause_array_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 | |
mp_integer | lower_bound |
mp_integer | upper_bound |
exprt | lower_offset_object |
exprt | upper_offset_object |
symbol_exprt | array_standin_variable |
symbol_exprt | lower_offset_variable |
symbol_exprt | upper_offset_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 302 of file code_contracts.h.
assigns_clause_array_targett::assigns_clause_array_targett | ( | const exprt & | object_ptr, |
code_contractst & | contract, | ||
messaget & | log_parameter, | ||
const irep_idt & | function_id | ||
) |
Definition at line 1263 of file code_contracts.cpp.
Implements assigns_clause_targett.
Definition at line 1386 of file code_contracts.cpp.
|
virtual |
Implements assigns_clause_targett.
Definition at line 1404 of file code_contracts.cpp.
|
virtual |
Implements assigns_clause_targett.
Definition at line 1353 of file code_contracts.cpp.
|
virtual |
Implements assigns_clause_targett.
Definition at line 1342 of file code_contracts.cpp.
|
protected |
Definition at line 323 of file code_contracts.h.
|
protected |
Definition at line 317 of file code_contracts.h.
|
protected |
Definition at line 320 of file code_contracts.h.
|
protected |
Definition at line 324 of file code_contracts.h.
|
protected |
Definition at line 318 of file code_contracts.h.
|
protected |
Definition at line 321 of file code_contracts.h.
|
protected |
Definition at line 325 of file code_contracts.h.