35 const irept &sizeof_type=expr.
find(ID_C_c_sizeof_type);
39 return static_cast<const typet &
>(sizeof_type);
41 else if(expr.
id()==ID_mult)
60 throw "malloc expected to have one operand";
95 tmp_size.
id()==ID_mult &&
113 if(alloc_size==elem_size)
114 object_type=tmp_type;
119 if(elements*elem_size==alloc_size)
133 if(object_type.
id()==ID_array &&
145 size_symbol.
mode=ID_C;
150 size=assignment.lhs();
162 value_symbol.
type=object_type;
163 value_symbol.
type.
set(
"#dynamic",
true);
164 value_symbol.
mode=ID_C;
170 if(object_type.
id()==ID_array)
176 rhs.
op0()=index_expr;
192 if(src.
id()==ID_typecast)
194 else if(src.
id()==ID_address_of)
197 if(op.
id()==ID_symbol &&
213 throw "va_arg_next expected to have one operand";
229 if(pos!=std::string::npos)
232 std::string base=
id2string(function_identifier)+
"::va_arg";
235 id=base+std::to_string(
237 std::string(
id2string(
id), base.size(), std::string::npos))+1);
256 if(src.
id()==ID_typecast)
261 else if(src.
id()==ID_address_of)
264 if(src.
op0().
id()==ID_index)
268 if(src.
op0().
op0().
id()==ID_string_constant &&
293 throw "printf expected to have at least one operand";
300 std::list<exprt> args;
302 for(
unsigned i=1; i<operands.size(); i++)
303 args.push_back(operands[i]);
308 if(format_string!=
"")
311 state.
source,
"printf", format_string, args);
319 throw "input expected to have at least two operands";
325 std::list<exprt> args;
327 for(
unsigned i=1; i<code.
operands().size(); i++)
344 throw "output expected to have at least two operands";
350 std::list<exprt> args;
352 for(
unsigned i=1; i<code.
operands().size(); i++)
371 if(code.
type().
id()!=ID_pointer)
372 throw "new expected to return pointer";
374 do_array=(code.
get(ID_statement)==ID_cpp_new_array);
383 do_array?
"dynamic_"+count_string+
"_array":
384 "dynamic_"+count_string+
"_value";
395 symbol.
type.
set(ID_size, size_arg);
401 symbol.
type.
set(
"#dynamic",
true);
416 rhs.move_to_operands(index_expr);
437 throw "symex_trace expects at least two arguments";
445 throw "CBMC_trace expects constant as first argument";
447 if(code.
arguments()[1].id()!=
"implicit_address_of" ||
448 code.
arguments()[1].operands().size()!=1 ||
449 code.
arguments()[1].op0().id()!=ID_string_constant)
451 throw "CBMC_trace expects string constant as second argument";
455 std::list<exprt> vars;
459 for(
unsigned j=2; j<code.
arguments().size(); j++)
475 exprt new_fc(ID_function, fc.type());
485 new_fc.move_to_operands(*it);
487 new_fc.set(ID_identifier, fc.op0().get(ID_identifier));
502 exprt new_fc(
"waitfor", fc.type());
504 if(fc.operands().size()!=4)
505 throw "waitfor expected to have four operands";
511 if(cycle_var.
id()!=ID_symbol)
512 throw "waitfor expects symbol as first operand but got "+
515 exprt new_cycle_var(cycle_var);
516 new_cycle_var.
id(
"waitfor_symbol");
521 new_fc.operands().resize(4);
522 new_fc.op0().swap(cycle_var);
523 new_fc.op1().swap(new_cycle_var);
524 new_fc.op2().swap(bound);
525 new_fc.op3().swap(predicate);
531 throw "unknown macro: "+
id2string(identifier);
virtual void do_simplify(exprt &expr)
The type of an expression.
irep_idt name
The unique identifier.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Linking: Zero Initialization.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
irep_idt get_string_argument_rec(const exprt &src)
irep_idt mode
Language mode.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
void copy_to_operands(const exprt &expr)
virtual void symex_gcc_builtin_va_arg_next(statet &state, const exprt &lhs, const side_effect_exprt &code)
virtual void symex_trace(statet &state, const code_function_callt &code)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
bool get_bool(const irep_namet &name) const
virtual void symex_macro(statet &state, const code_function_callt &code)
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
virtual void symex_printf(statet &state, const exprt &lhs, const exprt &rhs)
const irep_idt & id() const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
static unsigned dynamic_counter
const std::string get_option(const std::string &option) const
API to expression classes.
const irep_idt & get(const irep_namet &name) const
virtual void symex_input(statet &state, const codet &code)
const exprt & size() const
Base class for tree-like data structures with sharing.
#define forall_operands(it, expr)
irep_idt get_string_argument(const exprt &src, const namespacet &ns)
irep_idt get_symbol(const exprt &src)
bitvector_typet index_type()
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void clean_expr(exprt &expr, statet &state, bool write)
Operator to return the address of an object.
static typet c_sizeof_type_rec(const exprt &expr)
virtual void symex_fkt(statet &state, const code_function_callt &code)
void symex_assign_rec(statet &state, const code_assignt &code)
std::vector< exprt > operandst
virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)
bool has_prefix(const std::string &s, const std::string &prefix)
symbol_tablet & new_symbol_table
unsigned safe_string2unsigned(const std::string &str, int base)
typet type
Type 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)=0
virtual void symex_malloc(statet &state, const exprt &lhs, const side_effect_exprt &code)
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< exprt > &args)=0
irep_idt get_object_name() const
const source_locationt & source_location() const
const std::string & get_string(const irep_namet &name) const
#define Forall_operands(it, expr)
virtual void symex_cpp_delete(statet &state, const codet &code)
Expression to hold a symbol (variable)
A statement in a programming language.
#define CPROVER_MACRO_PREFIX
unsignedbv_typet unsigned_char_type()
const typet & subtype() const
virtual void symex_output(statet &state, const codet &code)
An expression containing a side effect.
int unsafe_string2int(const std::string &str, int base)
void make_typecast(const typet &_type)
const irept & find(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)=0
void reserve_operands(operandst::size_type n)
bool simplify(exprt &expr, const namespacet &ns)
symex_targett::sourcet source