cprover
|
Expression classes for byte-level operators. More...
#include "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 15 of file byte_operators.cpp.
References configt::ansi_c, config, configt::ansi_ct::endianness, configt::ansi_ct::IS_BIG_ENDIAN, and configt::ansi_ct::IS_LITTLE_ENDIAN.
Referenced by goto_symext::address_arithmetic(), value_set_dereferencet::build_reference_to(), boolbvt::convert_member(), value_set_dereferencet::memory_model_bytes(), goto_symext::parameter_assignments(), goto_symext::process_array_expr_rec(), 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 30 of file byte_operators.cpp.
References configt::ansi_c, config, configt::ansi_ct::endianness, configt::ansi_ct::IS_BIG_ENDIAN, and configt::ansi_ct::IS_LITTLE_ENDIAN.
Referenced by path_symext::assign_rec(), and rewrite_union().
|
inline |
Definition at line 111 of file byte_operators.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 118 of file byte_operators.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 53 of file byte_operators.h.
References exprt::operands().
Referenced by goto_symext::address_arithmetic(), path_symext::assign_rec(), build_object_descriptor_rec(), graphml_witnesst::convert_assign_rec(), boolbvt::convert_bitvector(), smt1_convt::convert_expr(), 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::process_array_expr(), goto_symext::process_array_expr_rec(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_node(), goto_symext::symex_assign_rec(), and goto_symext::symex_other().
|
inline |
Definition at line 59 of file byte_operators.h.
References exprt::operands().
|
inline |
Definition at line 80 of file byte_operators.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 87 of file byte_operators.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 218 of file byte_operators.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 225 of file byte_operators.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 157 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 163 of file byte_operators.h.
References exprt::operands().
|
inline |
Definition at line 187 of file byte_operators.h.
References irept::id(), and exprt::operands().
|
inline |
Definition at line 194 of file byte_operators.h.
References irept::id(), and exprt::operands().