CBMC
Public Member Functions | Private Member Functions | Private Attributes | List of all members
symex_assignt Class Reference

Functor for symex assignment. More...

#include <symex_assign.h>

+ Collaboration diagram for symex_assignt:

Public Member Functions

 symex_assignt (goto_symex_statet &state, symex_targett::assignment_typet assignment_type, const namespacet &ns, const symex_configt &symex_config, symex_targett &target)
 
void assign_symbol (const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
 Record the assignment of value rhs to variable lhs in state and add the equation to target: lhs#{n+1} == guard ? rhs#{m} : lhs#{n} where {n} and {m} denote the current L2 indexes of lhs and rhs respectively. More...
 
void assign_rec (const exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
 

Private Member Functions

void assign_from_struct (const ssa_exprt &lhs, const expr_skeletont &full_lhs, const struct_exprt &rhs, const exprt::operandst &guard)
 Assign a struct expression to a symbol. More...
 
void assign_non_struct_symbol (const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
 
template<bool use_update>
void assign_array (const index_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
 
template<bool use_update>
void assign_struct_member (const member_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
 
void assign_if (const if_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
 
void assign_typecast (const typecast_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
 
void assign_byte_extract (const byte_extract_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
 

Private Attributes

goto_symex_statet & state
 
symex_targett::assignment_typet assignment_type
 
const namespacet & ns
 
const symex_configt & symex_config
 
symex_targett & target
 

Detailed Description

Functor for symex assignment.

Definition at line 25 of file symex_assign.h.

Constructor & Destructor Documentation

◆ symex_assignt()

symex_assignt::symex_assignt ( goto_symex_statet &  state,
symex_targett::assignment_typet  assignment_type,
const namespacet &  ns,
const symex_configt &  symex_config,
symex_targett &  target 
)
inline

Definition at line 28 of file symex_assign.h.

Member Function Documentation

◆ assign_array()

template<bool use_update>
void symex_assignt::assign_array ( const index_exprt &  lhs,
const expr_skeletont &  full_lhs,
const exprt &  rhs,
exprt::operandst &  guard 
)
private
Template Parameters
use_updateuse update_exprt instead of with_exprt when building expressions that modify components of an array or a struct

Definition at line 253 of file symex_assign.cpp.

◆ assign_byte_extract()

void symex_assignt::assign_byte_extract ( const byte_extract_exprt &  lhs,
const expr_skeletont &  full_lhs,
const exprt &  rhs,
exprt::operandst &  guard 
)
private

Definition at line 369 of file symex_assign.cpp.

◆ assign_from_struct()

void symex_assignt::assign_from_struct ( const ssa_exprt &  lhs,
const expr_skeletont &  full_lhs,
const struct_exprt &  rhs,
const exprt::operandst &  guard 
)
private

Assign a struct expression to a symbol.

If symex_assignt::assign_symbol was used then we would assign the whole symbol, before extracting its components, with results like x = {1, 2}; x..field1 = x.field1; x..field2 = x.field2; This abbreviates the process, directly producing x..field1 = 1; x..field2 = 2;

Parameters
lhssymbol to assign (already renamed to L1)
full_lhsexpression skeleton corresponding to lhs, to be included in the result trace
rhsstruct expression to assign to lhs
guardguard conjuncts that must hold for this assignment to be made

Definition at line 128 of file symex_assign.cpp.

◆ assign_if()

void symex_assignt::assign_if ( const if_exprt &  lhs,
const expr_skeletont &  full_lhs,
const exprt &  rhs,
exprt::operandst &  guard 
)
private

Definition at line 352 of file symex_assign.cpp.

◆ assign_non_struct_symbol()

void symex_assignt::assign_non_struct_symbol ( const ssa_exprt &  lhs,
const expr_skeletont &  full_lhs,
const exprt &  rhs,
const exprt::operandst &  guard 
)
private

Definition at line 150 of file symex_assign.cpp.

◆ assign_rec()

void symex_assignt::assign_rec ( const exprt &  lhs,
const expr_skeletont &  full_lhs,
const exprt &  rhs,
exprt::operandst &  guard 
)

Definition at line 36 of file symex_assign.cpp.

◆ assign_struct_member()

template<bool use_update>
void symex_assignt::assign_struct_member ( const member_exprt &  lhs,
const expr_skeletont &  full_lhs,
const exprt &  rhs,
exprt::operandst &  guard 
)
private
Template Parameters
use_updateuse update_exprt instead of with_exprt when building expressions that modify components of an array or a struct

Definition at line 290 of file symex_assign.cpp.

◆ assign_symbol()

void symex_assignt::assign_symbol ( const ssa_exprt &  lhs,
const expr_skeletont &  full_lhs,
const exprt &  rhs,
const exprt::operandst &  guard 
)

Record the assignment of value rhs to variable lhs in state and add the equation to target: lhs#{n+1} == guard ? rhs#{m} : lhs#{n} where {n} and {m} denote the current L2 indexes of lhs and rhs respectively.

Definition at line 226 of file symex_assign.cpp.

◆ assign_typecast()

void symex_assignt::assign_typecast ( const typecast_exprt &  lhs,
const expr_skeletont &  full_lhs,
const exprt &  rhs,
exprt::operandst &  guard 
)
private

Definition at line 239 of file symex_assign.cpp.

Member Data Documentation

◆ assignment_type

symex_targett::assignment_typet symex_assignt::assignment_type
private

Definition at line 60 of file symex_assign.h.

◆ ns

const namespacet& symex_assignt::ns
private

Definition at line 61 of file symex_assign.h.

◆ state

goto_symex_statet& symex_assignt::state
private

Definition at line 59 of file symex_assign.h.

◆ symex_config

const symex_configt& symex_assignt::symex_config
private

Definition at line 62 of file symex_assign.h.

◆ target

symex_targett& symex_assignt::target
private

Definition at line 63 of file symex_assign.h.

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