CBMC
|
#include "bv_pointers.h"
#include <util/arith_tools.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/exception_utils.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <util/replace_expr.h>
#include <util/simplify_expr.h>
#include <solvers/prop/bdd_expr.h>
#include <solvers/prop/literal_expr.h>
Go to the source code of this file.
Classes | |
class | bv_endianness_mapt |
Map bytes according to the configured endianness. More... | |
Macros | |
#define | COMPACT_OBJECT_SIZE_EQ |
Functions | |
static bool | is_pointer_subtraction (const exprt &expr) |
static std::string | bits_to_string (const propt &prop, const bvt &bv) |
#define COMPACT_OBJECT_SIZE_EQ |
Definition at line 731 of file bv_pointers.cpp.
|
static |
Definition at line 610 of file bv_pointers.cpp.