Loading...

Searching...

No Matches

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:

[フレーム]

[legend]

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, const irep_idt &language_mode, 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.

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.

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_memoryt > shadow_memory

goto_symex_statet & state

symex_targett::assignment_typet assignment_type

const namespacet & ns

const symex_configt & symex_config

const irep_idt & language_mode

symex_targett & target

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,

const irep_idt & language_mode,

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_update use update_exprt instead of with_exprt when building expressions that modify components of an array or a struct

Definition at line 293 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 409 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: lhs symbol to assign (already renamed to L1)

full_lhs expression skeleton corresponding to lhs, to be included in the result trace

rhs struct expression to assign to lhs

guard guard 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 392 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 190 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_update use update_exprt instead of with_exprt when building expressions that modify components of an array or a struct

Definition at line 330 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 266 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 279 of file symex_assign.cpp.

Member Data Documentation

◆ assignment_type

symex_targett::assignment_typet symex_assignt::assignment_type

private

Definition at line 67 of file symex_assign.h.

◆ language_mode

const irep_idt& symex_assignt::language_mode

private

Definition at line 70 of file symex_assign.h.

◆ ns

const namespacet& symex_assignt::ns

private

Definition at line 68 of file symex_assign.h.

◆ shadow_memory

std::optional<shadow_memoryt> symex_assignt::shadow_memory

private

Definition at line 65 of file symex_assign.h.

◆ state

goto_symex_statet& symex_assignt::state

private

Definition at line 66 of file symex_assign.h.

◆ symex_config

const symex_configt& symex_assignt::symex_config

private

Definition at line 69 of file symex_assign.h.

◆ target

symex_targett& symex_assignt::target

private

Definition at line 71 of file symex_assign.h.

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

/home/runner/work/cbmc/cbmc/src/goto-symex/symex_assign.h
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_assign.cpp