symex_assign.cpp File Reference

#include <cassert>
#include <climits>
#include <goto-symex/engine/dynamic_allocation.h>
#include <goto-symex/scheduler/execution_state.h>
#include <goto-symex/engine/goto_symex.h>
#include <util/lang/c_types.h>
#include <util/symtab/cprover_prefix.h>
#include <util/expr/expr_util.h>
#include <util/base/i2string.h>
#include <util/message/message.h>
#include <util/base/usr_utils.h>
#include <irep2/irep2.h>
#include <util/irep/migrate.h>
#include <util/irep/std_expr.h>

Include dependency graph for symex_assign.cpp:

Functions
static bool	is_lvalue (const expr2tc &e)
	Whether e denotes a place whose address can be taken.
static bool	is_elementwise_literal (const expr2tc &e)
	A literal holding one lvalue per element: an array member, or a vector a dereference rebuilt lane by lane (#7907).

Function Documentation

is_elementwise_literal()

bool is_elementwise_literal ( const expr2tc & e )

static

A literal holding one lvalue per element: an array member, or a vector a dereference rebuilt lane by lane (#7907).

is_lvalue()

bool is_lvalue ( const expr2tc & e )

static

Whether e denotes a place whose address can be taken.

Dereference lowering can turn a member read through an untyped allocation into a value rebuilt from bytes, and that has no address.