cprover
assigns_clauset Class Reference

#include <assigns.h>

+ Collaboration diagram for assigns_clauset:

Public Member Functions

 assigns_clauset (const exprt &assigns, code_contractst &contract, const irep_idt function_id, messaget log_parameter)
 
 ~assigns_clauset ()
 
assigns_clause_targettadd_target (exprt target)
 
goto_programt init_block ()
 
goto_programt dead_stmts ()
 
goto_programt havoc_code ()
 
exprt alias_expression (const exprt &lhs)
 
exprt compatible_expression (const assigns_clauset &called_assigns)
 

Protected Attributes

const exprtassigns
 
std::vector< assigns_clause_targett * > targets
 
goto_programt standin_declarations
 
code_contractstparent
 
const irep_idt function_id
 
messaget log
 

Detailed Description

Definition at line 52 of file assigns.h.

Constructor & Destructor Documentation

◆ assigns_clauset()

assigns_clauset::assigns_clauset ( const exprt assigns,
code_contractst contract,
const irep_idt  function_id,
messaget  log_parameter 
)

Definition at line 119 of file assigns.cpp.

◆ ~assigns_clauset()

assigns_clauset::~assigns_clauset ( )

Definition at line 135 of file assigns.cpp.

Member Function Documentation

◆ add_target()

assigns_clause_targett * assigns_clauset::add_target ( exprt  target)

Definition at line 143 of file assigns.cpp.

◆ alias_expression()

exprt assigns_clauset::alias_expression ( const exprt lhs)

Definition at line 195 of file assigns.cpp.

◆ compatible_expression()

exprt assigns_clauset::compatible_expression ( const assigns_clauset called_assigns)

Definition at line 211 of file assigns.cpp.

◆ dead_stmts()

goto_programt assigns_clauset::dead_stmts ( )

Definition at line 170 of file assigns.cpp.

◆ havoc_code()

goto_programt assigns_clauset::havoc_code ( )

Definition at line 184 of file assigns.cpp.

◆ init_block()

goto_programt assigns_clauset::init_block ( )

Definition at line 156 of file assigns.cpp.

Member Data Documentation

◆ assigns

const exprt& assigns_clauset::assigns
protected

Definition at line 70 of file assigns.h.

◆ function_id

const irep_idt assigns_clauset::function_id
protected

Definition at line 76 of file assigns.h.

◆ log

messaget assigns_clauset::log
protected

Definition at line 77 of file assigns.h.

◆ parent

code_contractst& assigns_clauset::parent
protected

Definition at line 75 of file assigns.h.

◆ standin_declarations

goto_programt assigns_clauset::standin_declarations
protected

Definition at line 73 of file assigns.h.

◆ targets

std::vector<assigns_clause_targett *> assigns_clauset::targets
protected

Definition at line 72 of file assigns.h.


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