Go to the documentation of this file.
30 const irept &sizeof_type=expr.
find(ID_C_c_sizeof_type);
34 return static_cast<const typet &
>(sizeof_type);
36 else if(expr.
id()==ID_mult)
64 INVARIANT(function_symbol,
"function associated with allocation not found");
65 const irep_idt &mode = function_symbol->mode;
69 code.
type().
id() == ID_pointer &&
84 if(tmp_type.has_value())
88 const auto alloc_size = numeric_cast<mp_integer>(tmp_size);
90 if(!elem_size.has_value() || *elem_size==0)
94 !alloc_size.has_value() && tmp_size.
id() == ID_mult &&
112 else if(alloc_size.has_value())
114 if(*alloc_size == *elem_size)
115 object_type = *tmp_type;
118 mp_integer elements = *alloc_size / (*elem_size);
120 if(elements * (*elem_size) == *alloc_size)
128 if(!object_type.has_value())
135 object_type->id() == ID_array &&
147 size_symbol.
mode = mode;
148 size_symbol.
type.
set(ID_C_constant,
true);
149 size_symbol.
value = array_size;
154 array_size = assignment.
lhs();
166 value_symbol.
type = *object_type;
167 value_symbol.
type.
set(ID_C_dynamic,
true);
168 value_symbol.
mode = mode;
177 zero_init.
is_constant(),
"allocate expects constant as second argument");
181 const auto zero_value =
197 if(object_type->id() == ID_array)
229 if(lhs_type.
subtype().
id() != ID_pointer)
231 auto parameter_size =
size_of_expr(parameter_expr.type(), ns);
270 bool parameter_id_found =
false;
273 if(!parameter_id_found)
275 parameter_id_found = parameter == start_parameter;
279 va_arg_operands.push_back(
282 const std::size_t va_arg_size = va_arg_operands.
size();
295 va_array.
value = array;
297 array =
clean_expr(std::move(array), state,
false);
298 array = state.
rename(std::move(array),
ns).get();
304 rhs = state.
rename(std::move(rhs),
ns).get();
312 if(src.
id()==ID_typecast)
316 else if(src.
id()==ID_address_of)
320 if(
object.
id() == ID_index)
325 index_expr.array().id() == ID_string_constant &&
326 index_expr.index().is_zero())
328 const exprt &fmt_str = index_expr.array();
332 else if(
object.
id() == ID_string_constant)
352 if(operands.size() != 2)
356 if(second_op.
id() != ID_address_of)
363 if(
object.
id() != ID_index)
370 return index_expr.
array();
381 tmp_rhs = state.
rename(std::move(tmp_rhs),
ns).get();
385 std::list<exprt> args;
390 if(!va_args.has_value())
392 args.insert(args.end(), std::next(operands.begin()), operands.end());
398 *va_args = state.
rename(*va_args,
ns).get();
399 if(va_args->id() != ID_array)
406 for(
const auto &op : va_args->operands())
409 if(parameter.
id() == ID_address_of)
412 parameter = state.
rename(std::move(parameter),
ns).get();
415 args.push_back(std::move(parameter));
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);
489 (code.
get(ID_statement) == ID_cpp_new_array ||
490 code.
get(ID_statement) == ID_java_new_array_data);
499 do_array?
"dynamic_"+count_string+
"_array":
500 "dynamic_"+count_string+
"_value";
503 if(code.
get(ID_statement)==ID_cpp_new_array ||
504 code.
get(ID_statement)==ID_cpp_new)
506 else if(code.
get(ID_statement) == ID_java_new_array_data)
520 symbol.
type.
set(ID_C_dynamic,
true);
545 bool do_array=code.get(ID_statement)==ID_cpp_delete_array;
556 exprt new_fc(ID_function, fc.type());
568 new_fc.
set(ID_identifier, fc.op0().get(ID_identifier));
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static exprt conditional_cast(const exprt &expr, const typet &type)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const typet & subtype() const
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
#define Forall_operands(it, expr)
symex_nondet_generatort build_symex_nondet
Counter for nondet objects, which require unique names.
static unsigned dynamic_counter
A monotonically increasing index for each created dynamic object.
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
Fresh auxiliary symbol creation.
goto_programt::const_targett pc
virtual void symex_printf(statet &state, const exprt &rhs)
Symbolically execute an OTHER instruction that does a CPP printf
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
symex_target_equationt & target
The equation that this execution is building up.
typet type
Type of symbol.
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Central data structure: state.
The trinary if-then-else operator.
Various predicates over pointers in programs.
void simplify(const namespacet &ns)
virtual void symex_fkt(statet &state, const code_function_callt &code)
Symbolically execute a FUNCTION_CALL instruction for a function whose name starts with CPROVER_FKT_PR...
const irept & find(const irep_namet &name) const
virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)
Symbolically execute an assignment instruction that has a CPP new or new array or a Java new array on...
const string_constantt & to_string_constant(const exprt &expr)
Base class for all expressions.
irep_idt get_object_name() const
symex_targett::sourcet source
irep_idt base_name
Base (non-scoped) name.
static optionalt< 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...
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
unsignedbv_typet unsigned_char_type()
Expression to hold a symbol (variable)
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
bitvector_typet index_type()
void symex_assign(statet &state, const code_assignt &code)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
bool is_false() const
Return whether the expression is a constant representing false.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const exprt & size() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
std::vector< irep_idt > parameter_names
Expression Initialization.
call_stackt & call_stack()
irep_idt mode
Language mode.
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program being executed.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
static irep_idt get_string_argument_rec(const exprt &src)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const std::string & id2string(const irep_idt &d)
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
virtual void symex_cpp_delete(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP delete
static optionalt< typet > c_sizeof_type_rec(const exprt &expr)
#define forall_operands(it, expr)
#define SYMEX_DYNAMIC_PREFIX
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
#define PRECONDITION(CONDITION)
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.
virtual void symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
virtual void symex_input(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP input.
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.
bool simplify(exprt &expr, const namespacet &ns)
pointer_typet pointer_type(const typet &subtype)
const irep_idt & id() const
std::vector< exprt > operandst
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
nonstd::optional< T > optionalt
virtual void do_simplify(exprt &expr)
field_sensitivityt field_sensitivity
std::size_t get_width() const
bool is_zero() const
Return whether the expression is a constant representing 0.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Deprecated expression utility functions.
exprt value
Initial value of symbol.
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.
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
const irep_idt & get(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bool is_constant() const
Return whether the expression is a constant.
const symex_configt symex_config
The configuration to use for this symbolic execution.
static irep_idt get_string_argument(const exprt &src, const namespacet &ns)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
NODISCARD 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...
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Operator to return the address of an object.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
unsignedbv_typet size_type()
A codet representing an assignment in the program.
void reserve_operands(operandst::size_type n)
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const source_locationt & source_location() const
Array constructor from list of elements.
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 ...
irep_idt name
The unique identifier.
virtual void symex_output(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP output.
Wrapper for expressions or types which have been renamed up to a given level.
const irep_idt & get_value() const
#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(IRE...
An expression containing a side effect.
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(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 >> &args)
Record an output.
Data structure for representing an arbitrary statement in a program.