cprover
assigns_clause_targett Class Reference

A base class for assigns clause targets. More...

#include <assigns.h>

+ Collaboration diagram for assigns_clause_targett:

Public Member Functions

 assigns_clause_targett (const exprt &object, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
 
 ~assigns_clause_targett ()
 
std::vector< symbol_exprttemporary_declarations () const
 
exprt alias_expression (const exprt &lhs)
 
exprt compatible_expression (const assigns_clause_targett &called_target)
 
const exprtget_direct_pointer () const
 
goto_programtget_init_block ()
 

Static Public Member Functions

static exprt pointer_for (const exprt &object)
 

Protected Attributes

const exprt pointer_object
 
const code_contractstcontract
 
goto_programt init_block
 
messagetlog
 
symbol_exprt target
 
const irep_idttarget_id
 

Detailed Description

A base class for assigns clause targets.

Definition at line 22 of file assigns.h.

Constructor & Destructor Documentation

◆ assigns_clause_targett()

assigns_clause_targett::assigns_clause_targett ( const exprt object,
code_contractst contract,
messaget log_parameter,
const irep_idt function_id 
)

Definition at line 22 of file assigns.cpp.

◆ ~assigns_clause_targett()

assigns_clause_targett::~assigns_clause_targett ( )

Definition at line 53 of file assigns.cpp.

Member Function Documentation

◆ alias_expression()

exprt assigns_clause_targett::alias_expression ( const exprt lhs)

Definition at line 64 of file assigns.cpp.

◆ compatible_expression()

exprt assigns_clause_targett::compatible_expression ( const assigns_clause_targett called_target)

Definition at line 103 of file assigns.cpp.

◆ get_direct_pointer()

const exprt & assigns_clause_targett::get_direct_pointer ( ) const

Definition at line 109 of file assigns.cpp.

◆ get_init_block()

goto_programt & assigns_clause_targett::get_init_block ( )

Definition at line 114 of file assigns.cpp.

◆ pointer_for()

static exprt assigns_clause_targett::pointer_for ( const exprt object)
inlinestatic

Definition at line 38 of file assigns.h.

◆ temporary_declarations()

std::vector< symbol_exprt > assigns_clause_targett::temporary_declarations ( ) const

Definition at line 57 of file assigns.cpp.

Member Data Documentation

◆ contract

const code_contractst& assigns_clause_targett::contract
protected

Definition at line 45 of file assigns.h.

◆ init_block

goto_programt assigns_clause_targett::init_block
protected

Definition at line 46 of file assigns.h.

◆ log

messaget& assigns_clause_targett::log
protected

Definition at line 47 of file assigns.h.

◆ pointer_object

const exprt assigns_clause_targett::pointer_object
protected

Definition at line 44 of file assigns.h.

◆ target

symbol_exprt assigns_clause_targett::target
protected

Definition at line 48 of file assigns.h.

◆ target_id

const irep_idt& assigns_clause_targett::target_id
protected

Definition at line 49 of file assigns.h.


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