CBMC
|
Pointer Logic. More...
#include "pointer_offset_size.h"
#include "arith_tools.h"
#include "byte_operators.h"
#include "c_types.h"
#include "config.h"
#include "invariant.h"
#include "namespace.h"
#include "pointer_expr.h"
#include "simplify_expr.h"
#include "ssa_expr.h"
#include "std_expr.h"
Go to the source code of this file.
Functions | |
std::optional< mp_integer > | member_offset (const struct_typet &type, const irep_idt &member, const namespacet &ns) |
std::optional< mp_integer > | member_offset_bits (const struct_typet &type, const irep_idt &member, const namespacet &ns) |
std::optional< mp_integer > | pointer_offset_size (const typet &type, const namespacet &ns) |
Compute the size of a type in bytes, rounding up to full bytes. More... | |
std::optional< mp_integer > | pointer_offset_bits (const typet &type, const namespacet &ns) |
std::optional< exprt > | member_offset_expr (const member_exprt &member_expr, const namespacet &ns) |
std::optional< exprt > | member_offset_expr (const struct_typet &type, const irep_idt &member, const namespacet &ns) |
std::optional< exprt > | size_of_expr (const typet &type, const namespacet &ns) |
std::optional< mp_integer > | compute_pointer_offset (const exprt &expr, const namespacet &ns) |
std::optional< exprt > | get_subexpression_at_offset (const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns) |
std::optional< exprt > | get_subexpression_at_offset (const exprt &expr, const exprt &offset, const typet &target_type, const namespacet &ns) |
Pointer Logic.
Definition in file pointer_offset_size.cpp.
std::optional<mp_integer> compute_pointer_offset | ( | const exprt & | expr, |
const namespacet & | ns | ||
) |
Definition at line 496 of file pointer_offset_size.cpp.
std::optional<exprt> get_subexpression_at_offset | ( | const exprt & | expr, |
const exprt & | offset, | ||
const typet & | target_type, | ||
const namespacet & | ns | ||
) |
Definition at line 688 of file pointer_offset_size.cpp.
std::optional<exprt> get_subexpression_at_offset | ( | const exprt & | expr, |
const mp_integer & | offset_bytes, | ||
const typet & | target_type_raw, | ||
const namespacet & | ns | ||
) |
Definition at line 560 of file pointer_offset_size.cpp.
std::optional<mp_integer> member_offset | ( | const struct_typet & | type, |
const irep_idt & | member, | ||
const namespacet & | ns | ||
) |
Definition at line 25 of file pointer_offset_size.cpp.
std::optional<mp_integer> member_offset_bits | ( | const struct_typet & | type, |
const irep_idt & | member, | ||
const namespacet & | ns | ||
) |
Definition at line 66 of file pointer_offset_size.cpp.
std::optional<exprt> member_offset_expr | ( | const member_exprt & | member_expr, |
const namespacet & | ns | ||
) |
Definition at line 222 of file pointer_offset_size.cpp.
std::optional<exprt> member_offset_expr | ( | const struct_typet & | type, |
const irep_idt & | member, | ||
const namespacet & | ns | ||
) |
Definition at line 241 of file pointer_offset_size.cpp.
std::optional<mp_integer> pointer_offset_bits | ( | const typet & | type, |
const namespacet & | ns | ||
) |
Definition at line 102 of file pointer_offset_size.cpp.
std::optional<mp_integer> pointer_offset_size | ( | const typet & | type, |
const namespacet & | ns | ||
) |
Compute the size of a type in bytes, rounding up to full bytes.
Definition at line 91 of file pointer_offset_size.cpp.
std::optional<exprt> size_of_expr | ( | const typet & | type, |
const namespacet & | ns | ||
) |
Definition at line 287 of file pointer_offset_size.cpp.