cprover
|
Expression classes for byte-level operators. More...
#include "std_expr.h"
Go to the source code of this file.
Classes | |
class | byte_extract_exprt |
TO_BE_DOCUMENTED. More... | |
class | byte_extract_little_endian_exprt |
TO_BE_DOCUMENTED. More... | |
class | byte_extract_big_endian_exprt |
TO_BE_DOCUMENTED. More... | |
class | byte_update_exprt |
TO_BE_DOCUMENTED. More... | |
class | byte_update_little_endian_exprt |
TO_BE_DOCUMENTED. More... | |
class | byte_update_big_endian_exprt |
TO_BE_DOCUMENTED. More... | |
Functions | |
const byte_extract_exprt & | to_byte_extract_expr (const exprt &expr) |
byte_extract_exprt & | to_byte_extract_expr (exprt &expr) |
irep_idt | byte_extract_id () |
irep_idt | byte_update_id () |
const byte_extract_little_endian_exprt & | to_byte_extract_little_endian_expr (const exprt &expr) |
byte_extract_little_endian_exprt & | to_byte_extract_little_endian_expr (exprt &expr) |
const byte_extract_big_endian_exprt & | to_byte_extract_big_endian_expr (const exprt &expr) |
byte_extract_big_endian_exprt & | to_byte_extract_big_endian_expr (exprt &expr) |
const byte_update_exprt & | to_byte_update_expr (const exprt &expr) |
byte_update_exprt & | to_byte_update_expr (exprt &expr) |
const byte_update_little_endian_exprt & | to_byte_update_little_endian_expr (const exprt &expr) |
byte_update_little_endian_exprt & | to_byte_update_little_endian_expr (exprt &expr) |
const byte_update_big_endian_exprt & | to_byte_update_big_endian_expr (const exprt &expr) |
byte_update_big_endian_exprt & | to_byte_update_big_endian_expr (exprt &expr) |
Expression classes for byte-level operators.
Definition in file byte_operators.h.
irep_idt byte_extract_id | ( | ) |
Definition at line 16 of file byte_operators.cpp.
References configt::ansi_c, config, configt::ansi_ct::endianness, configt::ansi_ct::IS_BIG_ENDIAN, configt::ansi_ct::IS_LITTLE_ENDIAN, and UNREACHABLE.
Referenced by goto_symext::address_arithmetic(), value_set_dereferencet::build_reference_to(), boolbvt::convert_index(), boolbvt::convert_member(), value_set_dereferencet::memory_model_bytes(), goto_symext::parameter_assignments(), goto_symext::process_array_expr(), dereferencet::read_object(), rewrite_union(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), and goto_symext::symex_other().
irep_idt byte_update_id | ( | ) |
Definition at line 31 of file byte_operators.cpp.
References configt::ansi_c, config, configt::ansi_ct::endianness, configt::ansi_ct::IS_BIG_ENDIAN, configt::ansi_ct::IS_LITTLE_ENDIAN, and UNREACHABLE.
Referenced by rewrite_union().
|
inline |
Definition at line 110 of file byte_operators.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 117 of file byte_operators.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 52 of file byte_operators.h.
References exprt::operands().
Referenced by goto_symext::address_arithmetic(), adjust_byte_extract_rec(), build_object_descriptor_rec(), bv_pointerst::convert_address_of_rec(), graphml_witnesst::convert_assign_rec(), boolbvt::convert_bitvector(), smt2_convt::convert_expr(), bv_pointerst::convert_pointer_type(), flatten_byte_operators(), rw_range_sett::get_objects_address_of(), rw_range_sett::get_objects_rec(), goto_symext::havoc_rec(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_node(), and goto_symext::symex_assign_rec().
|
inline |
Definition at line 58 of file byte_operators.h.
References exprt::operands().
|
inline |
Definition at line 79 of file byte_operators.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 86 of file byte_operators.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 217 of file byte_operators.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 224 of file byte_operators.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 156 of file byte_operators.h.
References exprt::operands().
Referenced by boolbvt::convert_bitvector(), smt2_convt::convert_expr(), flatten_byte_operators(), and simplify_exprt::simplify_node().
|
inline |
Definition at line 162 of file byte_operators.h.
References exprt::operands().
|
inline |
Definition at line 186 of file byte_operators.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 193 of file byte_operators.h.
References irept::id(), and exprt::operands().