25 if(dest.
id()==ID_symbol)
41 else if(dest.
id()==ID_byte_extract_little_endian ||
42 dest.
id()==ID_byte_extract_big_endian)
46 else if(dest.
id()==ID_if)
58 else if(dest.
id()==ID_typecast)
62 else if(dest.
id()==ID_index)
66 else if(dest.
id()==ID_member)
85 if(statement==ID_expression)
89 else if(statement==ID_cpp_delete ||
90 statement==
"cpp_delete[]")
92 codet clean_code=code;
96 else if(statement==ID_free)
100 else if(statement==ID_printf)
102 codet clean_code=code;
106 else if(statement==ID_input)
108 codet clean_code(code);
112 else if(statement==ID_output)
114 codet clean_code(code);
118 else if(statement==ID_decl)
122 else if(statement==ID_nondet)
126 else if(statement==ID_asm)
130 else if(statement==ID_array_copy ||
131 statement==ID_array_replace)
142 "array_copy/array_replace takes two operands");
159 if(statement==ID_array_copy)
163 be.
type()=dest_array.type();
172 be.
type()=src_array.type();
181 else if(statement==ID_array_set)
205 if(array_expr.type().id() != ID_array)
225 else if(statement==ID_array_equal)
237 "array_equal expected to take three arguments");
257 else if(statement==ID_user_specified_predicate ||
258 statement==ID_user_specified_parameter_predicates ||
259 statement==ID_user_specified_return_predicates)
263 else if(statement==ID_fence)
267 else if(statement==ID_havoc_object)
270 "havoc_object must have one operand");
279 throw "unexpected statement: "+
id2string(statement);
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
const irep_idt & get_statement() const
exprt size_of_expr(const typet &type, const namespacet &ns)
virtual void memory_barrier(const exprt &guard, const sourcet &source)
const std::string & id2string(const irep_idt &d)
goto_programt::const_targett pc
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
The trinary if-then-else operator.
virtual void do_simplify(exprt &)
This class represents an instruction in the GOTO intermediate representation.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
const irep_idt & id() const
Expression classes for byte-level operators.
virtual void symex_other(statet &)
Operator to dereference a pointer.
symex_target_equationt & target
irep_idt byte_extract_id()
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
A side effect that returns a non-deterministically chosen value.
array constructor from single element
bitvector_typet index_type()
The boolean constant false.
virtual void symex_input(statet &, const codet &)
void symex_assign(statet &, const code_assignt &)
void process_array_expr(exprt &)
Given an expression, find the root object and the offset into it.
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.
virtual void symex_output(statet &, const codet &)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const codet & to_code(const exprt &expr)
virtual void symex_printf(statet &, const exprt &lhs, const exprt &rhs)
A statement in a programming language.
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
virtual void symex_cpp_delete(statet &, const codet &)
void make_typecast(const typet &_type)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
bitvector_typet char_type()
void add(const exprt &expr)
void havoc_rec(statet &, const guardt &, const exprt &)
symex_targett::sourcet source