cprover
assigns_clause_scalar_targett Class Reference

#include <code_contracts.h>

+ Inheritance diagram for assigns_clause_scalar_targett:
+ Collaboration diagram for assigns_clause_scalar_targett:

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_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 local_standin_variable
 
- 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 265 of file code_contracts.h.

Constructor & Destructor Documentation

◆ assigns_clause_scalar_targett()

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.

Member Function Documentation

◆ alias_expression()

exprt assigns_clause_scalar_targett::alias_expression ( const exprt lhs)
virtual

Implements assigns_clause_targett.

Definition at line 1059 of file code_contracts.cpp.

◆ compatible_expression()

exprt assigns_clause_scalar_targett::compatible_expression ( const assigns_clause_targett called_target)
virtual

Implements assigns_clause_targett.

Definition at line 1064 of file code_contracts.cpp.

◆ havoc_code()

goto_programt assigns_clause_scalar_targett::havoc_code ( source_locationt  location) const
virtual

Implements assigns_clause_targett.

Definition at line 1078 of file code_contracts.cpp.

◆ temporary_declarations()

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

Implements assigns_clause_targett.

Definition at line 1052 of file code_contracts.cpp.

Member Data Documentation

◆ local_standin_variable

symbol_exprt assigns_clause_scalar_targett::local_standin_variable
protected

Definition at line 280 of file code_contracts.h.


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