cprover
|
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"
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) |
Symbolic Execution of ANSI-C.
Definition in file value_set_dereference.cpp.
|
inlinestatic |
Definition at line 716 of file value_set_dereference.cpp.
References namespace_baset::follow_tag(), irept::get_string(), irept::id(), typet::subtype(), to_c_enum_tag_type(), and unsafe_string2unsigned().
Referenced by value_set_dereferencet::memory_model().
|
static |
Definition at line 730 of file value_set_dereference.cpp.
References irept::id().
Referenced by value_set_dereferencet::memory_model(), and value_set_dereferencet::memory_model_bytes().