dereference.cpp File Reference

#include <cassert>
#include <langapi/language_util.h>
#include <pointer-analysis/dereference.h>
#include <pointer-analysis/value_set.h>
#include <sstream>
#include <util/arith/arith_tools.h>
#include <util/expr/base_type.h>
#include <util/lang/c_misc.h>
#include <util/lang/c_types.h>
#include <util/config/config.h>
#include <util/symtab/cprover_prefix.h>
#include <util/expr/expr_util.h>
#include <util/base/i2string.h>
#include <irep2/irep2.h>
#include <irep2/irep2_utils.h>
#include <util/message/format.h>
#include <util/irep/migrate.h>
#include <util/base/prefix.h>
#include <util/symtab/pretty.h>
#include <util/symtab/rename.h>
#include <util/irep/std_expr.h>
#include <util/expr/type_byte_size.h>

Include dependency graph for dereference.cpp:

Classes
class	dereferencet::quantifier_scopet
	Records what a forall2t/exists2t binds while its body is walked, so the index fold in dereference_expr_nonscalar leaves the bound variable alone: the rename callback carries no quantifier context and would substitute the like-named program variable's SSA value (rename_quantified guards the same concern at the renaming layer, #7024). More...

Enumerations
enum	target_flags {   flag_src_scalar = 0x01 , flag_src_array = 0x02 , flag_src_struct = 0x04 , flag_src_union = 0x08 ,   flag_dst_scalar = 0x10 , flag_dst_struct = 0x20 , flag_dst_union = 0x40 , flag_is_const_offs = 0x80 ,   flag_is_dyn_offs = 0x100 }

Functions
static expr2tc	get_base_dereference (const expr2tc &e)
static expr2tc	replace_dyn_offset_with_zero (const expr2tc &e)
static expr2tc	distribute_steps_over_if (const expr2tc &e)
	Push member/index steps inside a conditional, so (c ?
static void	warn_unchecked_packed_alignment (const type2tc &structure)
static bool	is_aligned_member (const expr2tc &expr, const namespacet &ns)
static bool	is_vla (const array_type2t &arr)
static bool	same_type_ignoring_vla_sizes (const type2tc &a, const type2tc &b)
static bool	same_pointer_ignoring_vla_sizes (const type2tc &a, const type2tc &b)
static bool	is_struct_prefix (const struct_type2t &dt, const struct_type2t &ot)
static int	dst_flag_of (const type2tc &type)
	Which row of build_reference_rec's table the destination type selects.
static int	src_flag_of (const expr2tc &value)
	Which column the source value selects.
static bool	is_symex_dynamic_object (const std::string &id)
static bool	is_heap_object (const expr2tc &obj, const namespacet &ns)

Variables
static constexpr unsigned	max_array_ref_elements = 1u << 20
	The most elements construct_array_ref builds one by one.

Enumeration Type Documentation

target_flags

enum target_flags

Enumerator
flag_src_scalar
flag_src_array
flag_src_struct
flag_src_union
flag_dst_scalar
flag_dst_struct
flag_dst_union
flag_is_const_offs
flag_is_dyn_offs

Function Documentation

distribute_steps_over_if()

expr2tc distribute_steps_over_if ( const expr2tc & e )

static

Push member/index steps inside a conditional, so (c ?

a : b).f becomes c ? a.f : b.f. Returns e unchanged when there is no conditional to lift. Both forms denote the same object; the rewrite only moves the selection outside the access path.

dst_flag_of()

int dst_flag_of ( const type2tc & type )

static

Which row of build_reference_rec's table the destination type selects.

get_base_dereference()

expr2tc get_base_dereference ( const expr2tc & e )

inlinestatic

is_aligned_member()

bool is_aligned_member ( const expr2tc & expr, const namespacet & ns )

static

is_heap_object()

bool is_heap_object ( const expr2tc & obj, const namespacet & ns )

static

is_struct_prefix()

bool is_struct_prefix ( const struct_type2t & dt, const struct_type2t & ot )

static

is_symex_dynamic_object()

bool is_symex_dynamic_object ( const std::string & id )

static

is_vla()

bool is_vla ( const array_type2t & arr )

static

replace_dyn_offset_with_zero()

expr2tc replace_dyn_offset_with_zero ( const expr2tc & e )

inlinestatic

same_pointer_ignoring_vla_sizes()

bool same_pointer_ignoring_vla_sizes ( const type2tc & a, const type2tc & b )

static

same_type_ignoring_vla_sizes()

bool same_type_ignoring_vla_sizes ( const type2tc & a, const type2tc & b )

static

src_flag_of()

int src_flag_of ( const expr2tc & value )

static

Which column the source value selects.

warn_unchecked_packed_alignment()

void warn_unchecked_packed_alignment ( const type2tc & structure )

static

Variable Documentation

max_array_ref_elements

unsigned max_array_ref_elements = 1u << 20

staticconstexpr

The most elements construct_array_ref builds one by one.

A 2^18-element read takes about 20 s and 400 MB, growing linearly.