cprover
assigns_clauset Class Reference

#include <code_contracts.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 current_operation)
 
assigns_clause_targettadd_pointer_target (exprt current_operation)
 
goto_programt init_block (source_locationt location)
 
goto_programttemporary_declarations (source_locationt location, irep_idt function_name, irep_idt language_mode)
 
goto_programt dead_stmts (source_locationt location, irep_idt function_name, irep_idt language_mode)
 
goto_programt havoc_code (source_locationt location, irep_idt function_name, irep_idt language_mode)
 
exprt alias_expression (const exprt &lhs)
 
exprt compatible_expression (const assigns_clauset &called_assigns)
 

Protected Attributes

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

Detailed Description

Definition at line 328 of file code_contracts.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 1430 of file code_contracts.cpp.

◆ ~assigns_clauset()

assigns_clauset::~assigns_clauset ( )

Definition at line 1445 of file code_contracts.cpp.

Member Function Documentation

◆ add_pointer_target()

assigns_clause_targett * assigns_clauset::add_pointer_target ( exprt  current_operation)

Definition at line 1482 of file code_contracts.cpp.

◆ add_target()

assigns_clause_targett * assigns_clauset::add_target ( exprt  current_operation)

Definition at line 1453 of file code_contracts.cpp.

◆ alias_expression()

exprt assigns_clauset::alias_expression ( const exprt lhs)

Definition at line 1554 of file code_contracts.cpp.

◆ compatible_expression()

exprt assigns_clauset::compatible_expression ( const assigns_clauset called_assigns)

Definition at line 1580 of file code_contracts.cpp.

◆ dead_stmts()

goto_programt assigns_clauset::dead_stmts ( source_locationt  location,
irep_idt  function_name,
irep_idt  language_mode 
)

Definition at line 1520 of file code_contracts.cpp.

◆ havoc_code()

goto_programt assigns_clauset::havoc_code ( source_locationt  location,
irep_idt  function_name,
irep_idt  language_mode 
)

Definition at line 1537 of file code_contracts.cpp.

◆ init_block()

goto_programt assigns_clauset::init_block ( source_locationt  location)

Definition at line 1487 of file code_contracts.cpp.

◆ temporary_declarations()

goto_programt & assigns_clauset::temporary_declarations ( source_locationt  location,
irep_idt  function_name,
irep_idt  language_mode 
)

Definition at line 1501 of file code_contracts.cpp.

Member Data Documentation

◆ assigns_expr

const exprt& assigns_clauset::assigns_expr
protected

Definition at line 358 of file code_contracts.h.

◆ function_id

const irep_idt assigns_clauset::function_id
protected

Definition at line 364 of file code_contracts.h.

◆ log

messaget assigns_clauset::log
protected

Definition at line 365 of file code_contracts.h.

◆ parent

code_contractst& assigns_clauset::parent
protected

Definition at line 363 of file code_contracts.h.

◆ standin_declarations

goto_programt assigns_clauset::standin_declarations
protected

Definition at line 361 of file code_contracts.h.

◆ targets

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

Definition at line 360 of file code_contracts.h.


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