cprover
value_set_dereference.cpp File Reference

Symbolic Execution of ANSI-C. More...

#include "value_set_dereference.h"
#include <cassert>
#include <util/invariant.h>
#include <util/string2int.h>
#include <util/expr_util.h>
#include <util/base_type.h>
#include <util/arith_tools.h>
#include <util/rename.h>
#include <util/array_name.h>
#include <util/config.h>
#include <util/std_expr.h>
#include <util/cprover_prefix.h>
#include <util/pointer_offset_size.h>
#include <util/symbol_table.h>
#include <util/guard.h>
#include <util/options.h>
#include <util/pointer_predicates.h>
#include <util/byte_operators.h>
#include <util/ssa_expr.h>
#include <util/c_types.h>
#include <ansi-c/c_typecast.h>
#include <pointer-analysis/value_set.h>
#include <langapi/language_util.h>
#include "pointer_offset_sum.h"
Include dependency graph for value_set_dereference.cpp:

Go to the source code of this file.

Functions

static unsigned bv_width (const typet &type, const namespacet &ns)
 
static bool is_a_bv_type (const typet &type)
 

Detailed Description

Symbolic Execution of ANSI-C.

Definition in file value_set_dereference.cpp.

Function Documentation

§ bv_width()

static unsigned bv_width ( const typet type,
const namespacet ns 
)
inlinestatic

§ is_a_bv_type()

static bool is_a_bv_type ( const typet type)
static