CBMC
Loading...
Searching...
No Matches
Classes | Macros | Functions
bv_pointers.cpp File Reference
#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>
+ Include dependency graph for bv_pointers.cpp:

Go to the source code of this file.

Classes

  Map bytes according to the configured endianness. More...
 

Macros

 

Functions

 
static std::string  bits_to_string (const propt &prop, const bvt &bv)
 

Macro Definition Documentation

◆  COMPACT_OBJECT_SIZE_EQ

#define COMPACT_OBJECT_SIZE_EQ

Function Documentation

◆  bits_to_string()

static std::string bits_to_string ( const proptprop,
const bvtbv 
)
static

Definition at line 731 of file bv_pointers.cpp.

◆  is_pointer_subtraction()

static bool is_pointer_subtraction ( const exprtexpr )
static

Definition at line 610 of file bv_pointers.cpp.

AltStyle によって変換されたページ (->オリジナル) /