24 const irept &sizeof_type=expr.
find(ID_C_c_sizeof_type);
28 return static_cast<const typet &
>(sizeof_type);
30 else if(expr.
id()==ID_mult)
49 throw "allocate expected to have two operands";
59 INVARIANT(function_symbol,
"function associated with instruction not found");
60 const irep_idt &mode = function_symbol->mode;
87 tmp_size.
id()==ID_mult &&
105 if(alloc_size==elem_size)
106 object_type=tmp_type;
111 if(elements*elem_size==alloc_size)
125 if(object_type.
id()==ID_array &&
136 size_symbol.
mode = mode;
137 size_symbol.
type.
set(ID_C_constant,
true);
138 size_symbol.
value = size;
143 size=assignment.lhs();
155 value_symbol.
type=object_type;
156 value_symbol.
type.
set(ID_C_dynamic,
true);
157 value_symbol.
mode = mode;
166 throw "allocate expects constant as second argument";
184 throw "failed to zero initialize dynamic object";
195 if(object_type.
id()==ID_array)
217 if(src.
id()==ID_typecast)
219 else if(src.
id()==ID_address_of)
222 if(op.
id()==ID_symbol &&
238 throw "va_arg_next expected to have one operand";
254 if(
pos!=std::string::npos)
257 std::string base=
id2string(function_identifier)+
"::va_arg";
262 std::string(
id2string(
id), base.size(), std::string::npos))+1);
281 if(src.
id()==ID_typecast)
286 else if(src.
id()==ID_address_of)
289 if(src.
op0().
id()==ID_index)
293 if(src.
op0().
op0().
id()==ID_string_constant &&
317 throw "printf expected to have at least one operand";
324 std::list<exprt> args;
326 for(std::size_t i=1; i<operands.size(); i++)
327 args.push_back(operands[i]);
332 if(format_string!=
"")
335 state.
source,
"printf", format_string, args);
343 throw "input expected to have at least two operands";
349 std::list<exprt> args;
351 for(std::size_t i=1; i<code.
operands().size(); i++)
368 throw "output expected to have at least two operands";
374 std::list<exprt> args;
376 for(std::size_t i=1; i<code.
operands().size(); i++)
400 if(code.
type().
id()!=ID_pointer)
401 throw "new expected to return pointer";
404 (code.
get(ID_statement) == ID_cpp_new_array ||
405 code.
get(ID_statement) == ID_java_new_array_data);
414 do_array?
"dynamic_"+count_string+
"_array":
415 "dynamic_"+count_string+
"_value";
418 if(code.
get(ID_statement)==ID_cpp_new_array ||
419 code.
get(ID_statement)==ID_cpp_new)
421 else if(code.
get(ID_statement) == ID_java_new_array_data)
435 symbol.
type.
set(ID_C_dynamic,
true);
461 bool do_array=code.get(ID_statement)==ID_cpp_delete_array;
471 throw "symex_trace expects at least two arguments";
479 throw "CBMC_trace expects constant as first argument";
481 if(code.
arguments()[1].id()!=
"implicit_address_of" ||
482 code.
arguments()[1].operands().size()!=1 ||
483 code.
arguments()[1].op0().id()!=ID_string_constant)
485 throw "CBMC_trace expects string constant as second argument";
489 std::list<exprt> vars;
493 for(std::size_t j=2; j<code.
arguments().size(); j++)
510 exprt new_fc(ID_function, fc.type());
520 new_fc.move_to_operands(*it);
522 new_fc.set(ID_identifier, fc.op0().get(ID_identifier));
537 exprt new_fc(
"waitfor", fc.type());
539 if(fc.operands().size()!=4)
540 throw "waitfor expected to have four operands";
546 if(cycle_var.
id()!=ID_symbol)
547 throw "waitfor expects symbol as first operand but got "+
550 exprt new_cycle_var(cycle_var);
551 new_cycle_var.
id(
"waitfor_symbol");
556 new_fc.operands().resize(4);
557 new_fc.op0().swap(cycle_var);
558 new_fc.op1().swap(new_cycle_var);
559 new_fc.op2().swap(bound);
560 new_fc.op3().swap(predicate);
566 throw "unknown macro: "+
id2string(identifier);
The type of an expression.
irep_idt name
The unique identifier.
virtual void symex_gcc_builtin_va_arg_next(statet &, const exprt &lhs, const side_effect_exprt &)
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
irep_idt get_string_argument_rec(const exprt &src)
goto_programt::const_targett pc
virtual void symex_fkt(statet &, const code_function_callt &)
irep_idt mode
Language mode.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
void copy_to_operands(const exprt &expr)
void move_to_operands(exprt &expr)
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
just record input
exprt value
Initial value of symbol.
virtual void symex_macro(statet &, const code_function_callt &)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
virtual void do_simplify(exprt &)
bool get_bool(const irep_namet &name) const
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
#define INVARIANT(CONDITION, REASON)
#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(IRE...
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Expression Initialization.
const irep_idt & id() const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
virtual void symex_allocate(statet &, const exprt &lhs, const side_effect_exprt &)
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...
static unsigned dynamic_counter
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we're executing.
const std::string get_option(const std::string &option) const
symex_target_equationt & target
const irep_idt & get(const irep_namet &name) const
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
#define PRECONDITION(CONDITION)
bool has_prefix(const std::string &s, const std::string &prefix)
const exprt & size() const
Base class for tree-like data structures with sharing.
#define forall_operands(it, expr)
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
just record formatted output
irep_idt get_string_argument(const exprt &src, const namespacet &ns)
irep_idt get_symbol(const exprt &src)
bitvector_typet index_type()
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Operator to return the address of an object.
virtual void symex_trace(statet &, const code_function_callt &)
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &fmt, const std::list< exprt > &args)
just record output
static typet c_sizeof_type_rec(const exprt &expr)
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
std::vector< exprt > operandst
virtual void symex_input(statet &, const codet &)
void symex_assign(statet &, const code_assignt &)
unsigned safe_string2unsigned(const std::string &str, int base)
typet type
Type of symbol.
void clean_expr(exprt &, statet &, bool write)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
virtual void symex_output(statet &, const codet &)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
irep_idt get_object_name() const
const source_locationt & source_location() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
const std::string & get_string(const irep_namet &name) const
#define Forall_operands(it, expr)
virtual void symex_printf(statet &, const exprt &rhs)
Expression to hold a symbol (variable)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
A statement in a programming language.
#define CPROVER_MACRO_PREFIX
unsignedbv_typet unsigned_char_type()
const typet & subtype() const
An expression containing a side effect.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
int unsafe_string2int(const std::string &str, int base)
virtual void symex_cpp_delete(statet &, const codet &)
void make_typecast(const typet &_type)
const irept & find(const irep_namet &name) const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void set(const irep_namet &name, const irep_idt &value)
void reserve_operands(operandst::size_type n)
nondet_symbol_exprt build_symex_nondet(typet &type)
bool simplify(exprt &expr, const namespacet &ns)
symex_targett::sourcet source