25 if(dest.
id()==ID_symbol)
42 else if(dest.
id()==ID_byte_extract_little_endian ||
43 dest.
id()==ID_byte_extract_big_endian)
47 else if(dest.
id()==ID_if)
59 else if(dest.
id()==ID_typecast)
63 else if(dest.
id()==ID_index)
67 else if(dest.
id()==ID_member)
86 if(statement==ID_expression)
90 else if(statement==ID_cpp_delete ||
91 statement==
"cpp_delete[]")
93 codet clean_code=code;
97 else if(statement==ID_free)
101 else if(statement==ID_printf)
103 codet clean_code=code;
107 else if(statement==ID_input)
109 codet clean_code(code);
113 else if(statement==ID_output)
115 codet clean_code(code);
119 else if(statement==ID_decl)
123 else if(statement==ID_nondet)
127 else if(statement==ID_asm)
131 else if(statement==ID_array_copy ||
132 statement==ID_array_replace)
143 "array_copy/array_replace takes two operands");
160 if(statement==ID_array_copy)
164 be.
type()=dest_array.type();
173 be.
type()=src_array.type();
182 else if(statement==ID_array_set)
206 if(array_expr.type().id() != ID_array)
226 else if(statement==ID_array_equal)
238 "array_equal expected to take three arguments");
258 else if(statement==ID_user_specified_predicate ||
259 statement==ID_user_specified_parameter_predicates ||
260 statement==ID_user_specified_return_predicates)
264 else if(statement==ID_fence)
268 else if(statement==ID_havoc_object)
271 "havoc_object must have one operand");
280 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()
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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.
virtual void symex_printf(statet &, 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