Go to the documentation of this file.
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_printf)
99 codet clean_code=code;
103 else if(statement==ID_input)
105 codet clean_code(code);
109 else if(statement==ID_output)
111 codet clean_code(code);
115 else if(statement==ID_decl)
119 else if(statement==ID_nondet)
123 else if(statement==ID_asm)
127 else if(statement==ID_array_copy ||
128 statement==ID_array_replace)
139 "expected array_copy/array_replace statement to have two operands");
156 if(statement==ID_array_copy)
178 else if(statement==ID_array_set)
189 "expected array_set statement to have two operands");
204 if(array_expr.
type().
id() != ID_array)
224 else if(statement==ID_array_equal)
236 "expected array_equal statement to have three operands");
256 else if(statement==ID_user_specified_predicate ||
257 statement==ID_user_specified_parameter_predicates ||
258 statement==ID_user_specified_return_predicates)
262 else if(statement==ID_fence)
266 else if(statement==ID_havoc_object)
270 "expected havoc_object statement to have one operand");
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const typet & subtype() const
void symex_assign(statet &, const code_assignt &)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
void process_array_expr(exprt &)
Given an expression, find the root object and the offset into it.
goto_programt::const_targett pc
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
symex_target_equationt & target
Operator to dereference a pointer.
void add(const exprt &expr)
The trinary if-then-else operator.
void clean_expr(exprt &, statet &, bool write)
Base class for all expressions.
symex_targett::sourcet source
virtual void do_simplify(exprt &)
virtual void symex_printf(statet &, const exprt &rhs)
bool is_true() const
Return whether the expression is a constant representing true.
bitvector_typet index_type()
#define UNREACHABLE
This should be used to mark dead code.
irep_idt byte_extract_id()
typet & type()
Return the type of the expression.
virtual void symex_output(statet &, const codet &)
Expression classes for byte-level operators.
virtual void symex_cpp_delete(statet &, const codet &)
exprt size_of_expr(const typet &type, const namespacet &ns)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Array constructor from single element.
virtual void symex_other(statet &)
const irep_idt & id() const
The Boolean constant false.
bitvector_typet char_type()
A side_effect_exprt that returns a non-deterministically chosen value.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
A codet representing an assignment in the program.
const irep_idt & get_statement() const
virtual void symex_input(statet &, const codet &)
This class represents an instruction in the GOTO intermediate representation.
void havoc_rec(statet &, const guardt &, const exprt &)
Data structure for representing an arbitrary statement in a program.