cprover
assigns_clause_struct_targett Class Reference

#include <code_contracts.h>

+ Inheritance diagram for assigns_clause_struct_targett:
+ Collaboration diagram for assigns_clause_struct_targett:

Public Member Functions

 assigns_clause_struct_targett (const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
 
std::vector< symbol_exprttemporary_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
 
- Public Member Functions inherited from assigns_clause_targett
 assigns_clause_targett (target_type type, const exprt object_ptr, const code_contractst &contract, messaget &log_parameter)
 
virtual ~assigns_clause_targett ()
 
const exprtget_direct_pointer () const
 
goto_programtget_init_block ()
 

Protected Attributes

symbol_exprt main_struct_standin
 
std::vector< symbol_exprtlocal_standin_variables
 
- Protected Attributes inherited from assigns_clause_targett
const exprt pointer_object
 
const code_contractstcontract
 
goto_programt init_block
 
messagetlog
 

Additional Inherited Members

- Public Types inherited from assigns_clause_targett
enum  target_type { Scalar, Struct, Array }
 
- Static Public Member Functions inherited from assigns_clause_targett
static exprt pointer_for (const exprt &exp)
 
- Public Attributes inherited from assigns_clause_targett
const target_type target_type
 

Detailed Description

Definition at line 283 of file code_contracts.h.

Constructor & Destructor Documentation

◆ assigns_clause_struct_targett()

assigns_clause_struct_targett::assigns_clause_struct_targett ( const exprt object_ptr,
code_contractst contract,
messaget log_parameter,
const irep_idt function_id 
)

Definition at line 1093 of file code_contracts.cpp.

Member Function Documentation

◆ alias_expression()

exprt assigns_clause_struct_targett::alias_expression ( const exprt lhs)
virtual

Implements assigns_clause_targett.

Definition at line 1179 of file code_contracts.cpp.

◆ compatible_expression()

exprt assigns_clause_struct_targett::compatible_expression ( const assigns_clause_targett called_target)
virtual

Implements assigns_clause_targett.

Definition at line 1206 of file code_contracts.cpp.

◆ havoc_code()

goto_programt assigns_clause_struct_targett::havoc_code ( source_locationt  location) const
virtual

Implements assigns_clause_targett.

Definition at line 1248 of file code_contracts.cpp.

◆ temporary_declarations()

std::vector< symbol_exprt > assigns_clause_struct_targett::temporary_declarations ( ) const
virtual

Implements assigns_clause_targett.

Definition at line 1174 of file code_contracts.cpp.

Member Data Documentation

◆ local_standin_variables

std::vector<symbol_exprt> assigns_clause_struct_targett::local_standin_variables
protected

Definition at line 299 of file code_contracts.h.

◆ main_struct_standin

symbol_exprt assigns_clause_struct_targett::main_struct_standin
protected

Definition at line 298 of file code_contracts.h.


The documentation for this class was generated from the following files: