Go to the documentation of this file.
25 const irept &sizeof_type=expr.
find(ID_C_c_sizeof_type);
29 return static_cast<const typet &>(sizeof_type);
31 else if(expr.
id()==ID_mult)
59 INVARIANT(function_symbol,
"function associated with allocation not found");
60 const irep_idt &mode = function_symbol->mode;
64 code.
type().
id() == ID_pointer &&
85 if(!elem_size.has_value() || *elem_size==0)
89 tmp_size.
id()==ID_mult &&
107 if(alloc_size == *elem_size)
108 object_type=tmp_type;
111 mp_integer elements = alloc_size / (*elem_size);
113 if(elements * (*elem_size) == alloc_size)
127 if(object_type.
id()==ID_array &&
138 size_symbol.
mode = mode;
139 size_symbol.
type.
set(ID_C_constant,
true);
140 size_symbol.
value = array_size;
145 array_size = assignment.lhs();
157 value_symbol.
type=object_type;
158 value_symbol.
type.
set(ID_C_dynamic,
true);
159 value_symbol.
mode = mode;
168 zero_init.
is_constant(),
"allocate expects constant as second argument");
172 const auto zero_value =
187 if(object_type.
id()==ID_array)
209 if(src.
id()==ID_typecast)
211 else if(src.
id()==ID_address_of)
214 if(op.
id()==ID_symbol &&
247 if(
pos!=std::string::npos)
250 std::string base=
id2string(function_identifier)+
"::va_arg";
255 std::string(
id2string(
id), base.size(), std::string::npos))+1);
264 rhs.make_typecast(lhs.
type());
274 if(src.
id()==ID_typecast)
279 else if(src.
id()==ID_address_of)
282 if(src.
op0().
id()==ID_index)
287 index_expr.array().id() == ID_string_constant &&
288 index_expr.index().is_zero())
290 const exprt &fmt_str = index_expr.array();
317 std::list<exprt> args;
319 for(std::size_t i=1; i<operands.size(); i++)
320 args.push_back(operands[i]);
325 if(format_string!=
"")
328 state.
source,
"printf", format_string, args);
341 std::list<exprt> args;
343 for(std::size_t i=1; i<code.
operands().size(); i++)
365 std::list<exprt> args;
367 for(std::size_t i=1; i<code.
operands().size(); i++)
396 (code.
get(ID_statement) == ID_cpp_new_array ||
397 code.
get(ID_statement) == ID_java_new_array_data);
406 do_array?
"dynamic_"+count_string+
"_array":
407 "dynamic_"+count_string+
"_value";
410 if(code.
get(ID_statement)==ID_cpp_new_array ||
411 code.
get(ID_statement)==ID_cpp_new)
413 else if(code.
get(ID_statement) == ID_java_new_array_data)
420 exprt size_arg = static_cast<const exprt &>(code.
find(ID_size));
427 symbol.
type.
set(ID_C_dynamic,
true);
452 bool do_array=code.get(ID_statement)==ID_cpp_delete_array;
464 numeric_cast<mp_integer>(code.
arguments()[0]);
466 maybe_debug.has_value(),
"CBMC_trace expects constant as first argument");
467 debug_lvl = maybe_debug.value();
470 code.
arguments()[1].id() ==
"implicit_address_of" &&
471 code.
arguments()[1].operands().size() == 1 &&
472 code.
arguments()[1].op0().id() == ID_string_constant,
473 "CBMC_trace expects string constant as second argument");
477 std::list<exprt> vars;
481 for(std::size_t j=2; j<code.
arguments().size(); j++)
499 exprt new_fc(ID_function, fc.type());
509 new_fc.move_to_operands(*it);
511 new_fc.set(ID_identifier, fc.op0().get(ID_identifier));
525 exprt new_fc(
"waitfor", fc.type());
527 if(fc.operands().size()!=4)
528 throw "waitfor expected to have four operands";
534 if(cycle_var.
id()!=ID_symbol)
535 throw "waitfor expects symbol as first operand but got "+
538 exprt new_cycle_var(cycle_var);
539 new_cycle_var.
id(
"waitfor_symbol");
544 new_fc.operands().resize(4);
545 new_fc.op0().swap(cycle_var);
546 new_fc.op1().swap(new_cycle_var);
547 new_fc.op2().swap(bound);
548 new_fc.op3().swap(predicate);
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
static typet c_sizeof_type_rec(const exprt &expr)
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
const typet & subtype() const
#define Forall_operands(it, expr)
void symex_assign(statet &, const code_assignt &)
irep_idt get_symbol(const exprt &src)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
static unsigned dynamic_counter
The type of an expression, extends irept.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
symex_target_equationt & target
typet type
Type of symbol.
The NIL type, i.e., an invalid type, no value.
void clean_expr(exprt &, statet &, bool write)
const irept & find(const irep_namet &name) const
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
virtual void symex_macro(statet &, const code_function_callt &)
Base class for all expressions.
irep_idt get_object_name() const
symex_targett::sourcet source
irep_idt base_name
Base (non-scoped) name.
virtual void do_simplify(exprt &)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Internally generated symbol table entry.
unsignedbv_typet unsigned_char_type()
virtual void symex_printf(statet &, const exprt &rhs)
Expression to hold a symbol (variable)
bitvector_typet index_type()
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
virtual void symex_trace(statet &, const code_function_callt &)
bool is_false() const
Return whether the expression is a constant representing false.
symex_nondet_generatort build_symex_nondet
const exprt & size() const
#define CPROVER_MACRO_PREFIX
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.
bool get_bool(const irep_namet &name) const
virtual void symex_output(statet &, const codet &)
virtual void symex_cpp_delete(statet &, const codet &)
irep_idt mode
Language mode.
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we're executing.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
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.
#define forall_operands(it, expr)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
irep_idt get_string_argument(const exprt &src, const namespacet &ns)
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
unsigned safe_string2unsigned(const std::string &str, int base)
bool is_zero() const
Return whether the expression is a constant representing 0.
irep_idt get_string_argument_rec(const exprt &src)
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.
const std::string & get_string(const irep_namet &name) const
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.
virtual void symex_allocate(statet &, const exprt &lhs, const side_effect_exprt &)
const irep_idt & get(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
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.
virtual void symex_cpp_new(statet &, const exprt &lhs, const side_effect_exprt &)
Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes.
const symex_configt symex_config
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< exprt > &args)
Record an output.
virtual void symex_gcc_builtin_va_arg_next(statet &, const exprt &lhs, const side_effect_exprt &)
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual void symex_fkt(statet &, const code_function_callt &)
bool has_prefix(const std::string &s, const std::string &prefix)
Base class for tree-like data structures with sharing.
Operator to return the address of an object.
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
A codet representing an assignment in the program.
void reserve_operands(operandst::size_type n)
virtual void symex_input(statet &, const codet &)
const source_locationt & source_location() const
irep_idt name
The unique identifier.
#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.
Data structure for representing an arbitrary statement in a program.
#define CHECK_RETURN(CONDITION)