CBMC
symex_assignt Class Reference

Functor for symex assignment. More...

#include <symex_assign.h>

+ Collaboration diagram for symex_assignt:

Public Member Functions

 symex_assignt (std::optional< shadow_memoryt > shadow_memory, 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

std::optional< shadow_memorytshadow_memory
 
goto_symex_statetstate
 
symex_targett::assignment_typet assignment_type
 
const namespacetns
 
const symex_configtsymex_config
 
symex_targetttarget
 

Detailed Description

Functor for symex assignment.

Definition at line 27 of file symex_assign.h.

Constructor & Destructor Documentation

◆ symex_assignt()

symex_assignt::symex_assignt ( std::optional< shadow_memoryt shadow_memory,
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 30 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 287 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 403 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 165 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 386 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 187 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 58 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 324 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 260 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 273 of file symex_assign.cpp.

Member Data Documentation

◆ assignment_type

symex_targett::assignment_typet symex_assignt::assignment_type
private

Definition at line 65 of file symex_assign.h.

◆ ns

const namespacet& symex_assignt::ns
private

Definition at line 66 of file symex_assign.h.

◆ shadow_memory

std::optional<shadow_memoryt> symex_assignt::shadow_memory
private

Definition at line 63 of file symex_assign.h.

◆ state

goto_symex_statet& symex_assignt::state
private

Definition at line 64 of file symex_assign.h.

◆ symex_config

const symex_configt& symex_assignt::symex_config
private

Definition at line 67 of file symex_assign.h.

◆ target

symex_targett& symex_assignt::target
private

Definition at line 68 of file symex_assign.h.


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