38 for(
const auto &op : expr.
operands())
60 std::optional<typet> object_type;
126 if(!object_type.has_value())
141 "dynamic_object_size",
173 zero_init.is_constant(),
"allocate expects constant as second argument");
293 array =
clean_expr(std::move(array), state,
false);
294 array = state.
rename(std::move(array),
ns).get();
300 rhs = state.
rename(std::move(rhs),
ns).get();
346 if(operands.size() != 2)
379 std::list<exprt> args;
382 std::optional<exprt> va_args =
get_va_args(operands);
384 if(!va_args.has_value())
386 args.insert(args.end(), std::next(operands.begin()), operands.end());
392 *va_args = state.
rename(*va_args,
ns).get();
406 for(
const auto &op : va_args->operands())
422 if(!format_string.
empty())
425 state.
source,
"printf", format_string, args);
436 std::list<exprt> args;
438 for(std::size_t i=1; i<code.
operands().size(); i++)
442 args.emplace_back(std::move(
l2_arg));
457 std::list<renamedt<exprt, L2>> args;
459 for(std::size_t i=1; i<code.
operands().size(); i++)
464 args.emplace_back(
l2_arg);
484 std::optional<typet> type;
509 (
do_array ?
"dynamic_array" :
"dynamic_value"),
pointer_typet pointer_type(const typet &subtype)
unsignedbv_typet unsigned_char_type()
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Array constructor from list of elements.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
std::vector< irep_idt > parameter_names
Central data structure: state.
call_stackt & call_stack()
renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
field_sensitivityt field_sensitivity
symex_targett::sourcet source
const symbol_table_baset & outer_symbol_table
The symbol table associated with the goto-program being executed.
virtual void symex_input(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP input.
path_storaget & path_storage
Symbolic execution paths to be resumed later.
symex_target_equationt & target
The equation that this execution is building up.
virtual void symex_cpp_delete(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP delete
virtual void symex_allocate(statet &state, const exprt &lhs, const side_effect_exprt &code)
Symbolically execute an assignment instruction that has an allocate on the right hand side.
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
shadow_memoryt shadow_memory
Shadow memory instrumentation API.
virtual void symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
void symex_assign(statet &state, const exprt &lhs, const exprt &rhs)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
virtual void symex_printf(statet &state, const exprt &rhs)
Symbolically execute an OTHER instruction that does a CPP printf
virtual void symex_output(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP output.
virtual void do_simplify(exprt &expr)
virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)
Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes.
const symex_configt symex_config
The configuration to use for this symbolic execution.
The trinary if-then-else operator.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
symex_nondet_generatort build_symex_nondet
Counter for nondet objects, which require unique names.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
void symex_field_dynamic_init(goto_symex_statet &state, const exprt &expr, const side_effect_exprt &code)
Initialize global-scope shadow memory for dynamically allocated memory.
An expression containing a side effect.
Expression to hold a symbol (variable)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
Record formatted output.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 > > &args)
Record an output.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(I...
const std::string & id2string(const irep_idt &d)
Storage of symbolic execution paths to resume.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
bool simplify(exprt &expr, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const string_constantt & to_string_constant(const exprt &expr)
goto_programt::const_targett pc
static std::optional< exprt > get_va_args(const exprt::operandst &operands)
Return an expression if operands fulfills all criteria that we expect of the expression to be a varia...
static std::optional< typet > c_sizeof_type_rec(const exprt &expr)
static irep_idt get_string_argument_rec(const exprt &src)
static exprt va_list_entry(const irep_idt ¶meter, const pointer_typet &lhs_type, const namespacet &ns)
Construct an entry for the var args array.
static irep_idt get_string_argument(const exprt &src, const namespacet &ns)