cprover
assigns_clause_targett Class Referenceabstract

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

#include <code_contracts.h>

+ Inheritance diagram for assigns_clause_targett:
+ Collaboration diagram for assigns_clause_targett:

Public Types

enum  target_type { Scalar, Struct, Array }
 

Public Member Functions

 assigns_clause_targett (target_type type, const exprt object_ptr, const code_contractst &contract, messaget &log_parameter)
 
virtual ~assigns_clause_targett ()
 
virtual std::vector< symbol_exprttemporary_declarations () const =0
 
virtual exprt alias_expression (const exprt &lhs)=0
 
virtual exprt compatible_expression (const assigns_clause_targett &called_target)=0
 
virtual goto_programt havoc_code (source_locationt location) const =0
 
const exprtget_direct_pointer () const
 
goto_programtget_init_block ()
 

Static Public Member Functions

static exprt pointer_for (const exprt &exp)
 

Public Attributes

const target_type target_type
 

Protected Attributes

const exprt pointer_object
 
const code_contractstcontract
 
goto_programt init_block
 
messagetlog
 

Detailed Description

A base class for assigns clause targets.

Definition at line 205 of file code_contracts.h.

Member Enumeration Documentation

◆ target_type

Enumerator
Scalar 
Struct 
Array 

Definition at line 208 of file code_contracts.h.

Constructor & Destructor Documentation

◆ assigns_clause_targett()

assigns_clause_targett::assigns_clause_targett ( target_type  type,
const exprt  object_ptr,
const code_contractst contract,
messaget log_parameter 
)
inline

Definition at line 215 of file code_contracts.h.

◆ ~assigns_clause_targett()

virtual assigns_clause_targett::~assigns_clause_targett ( )
inlinevirtual

Definition at line 231 of file code_contracts.h.

Member Function Documentation

◆ alias_expression()

virtual exprt assigns_clause_targett::alias_expression ( const exprt lhs)
pure virtual

◆ compatible_expression()

virtual exprt assigns_clause_targett::compatible_expression ( const assigns_clause_targett called_target)
pure virtual

◆ get_direct_pointer()

const exprt& assigns_clause_targett::get_direct_pointer ( ) const
inline

Definition at line 241 of file code_contracts.h.

◆ get_init_block()

goto_programt& assigns_clause_targett::get_init_block ( )
inline

Definition at line 246 of file code_contracts.h.

◆ havoc_code()

virtual goto_programt assigns_clause_targett::havoc_code ( source_locationt  location) const
pure virtual

◆ pointer_for()

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

Definition at line 251 of file code_contracts.h.

◆ temporary_declarations()

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

Member Data Documentation

◆ contract

const code_contractst& assigns_clause_targett::contract
protected

Definition at line 260 of file code_contracts.h.

◆ init_block

goto_programt assigns_clause_targett::init_block
protected

Definition at line 261 of file code_contracts.h.

◆ log

messaget& assigns_clause_targett::log
protected

Definition at line 262 of file code_contracts.h.

◆ pointer_object

const exprt assigns_clause_targett::pointer_object
protected

Definition at line 259 of file code_contracts.h.

◆ target_type


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