28 const goto_programt::instructiont &instruction=*state.
source.
pc;
34 if(statement==ID_expression)
38 else if(statement==ID_cpp_delete ||
39 statement==
"cpp_delete[]")
41 codet clean_code=code;
45 else if(statement==ID_free)
49 else if(statement==ID_printf)
51 codet clean_code=code;
55 else if(statement==ID_input)
57 codet clean_code(code);
61 else if(statement==ID_output)
63 codet clean_code(code);
67 else if(statement==ID_decl)
71 else if(statement==ID_nondet)
75 else if(statement==ID_asm)
79 else if(statement==ID_array_copy ||
80 statement==ID_array_replace)
84 codet clean_code(code);
99 clean_code.op0().type().id()==ID_empty)
102 clean_code.op0()=clean_code.op0().op0();
107 clean_code.op1().type().id()==ID_empty)
110 clean_code.op1()=clean_code.op1().op0();
120 clean_code.op1().type(),
ns) ||
121 !op0_offset.is_zero() || !op1_offset.is_zero())
125 if(statement==ID_array_copy)
127 be.
op()=clean_code.
op1();
129 be.
type()=clean_code.op0().type();
132 if(!op0_offset.is_zero())
138 clean_code.op0().type());
139 clean_code.
op0()=op0;
145 be.
op()=clean_code.
op0();
147 be.
type()=clean_code.op1().type();
150 if(!op1_offset.is_zero())
156 clean_code.op1().type());
157 clean_code.
op1()=op1;
163 assignment.
lhs()=clean_code.
op0();
164 assignment.
rhs()=clean_code.
op1();
167 else if(statement==ID_array_set)
171 codet clean_code(code);
182 clean_code.op0().type().id()==ID_empty)
183 clean_code.op0()=clean_code.op0().op0();
191 if(op0_type.id()!=ID_array)
192 throw "array_set expects array operand";
198 clean_code.op1().type(),
ns))
199 clean_code.op1().make_typecast(array_type.
subtype());
202 assignment.
lhs()=clean_code.
op0();
206 else if(statement==ID_user_specified_predicate ||
207 statement==ID_user_specified_parameter_predicates ||
208 statement==ID_user_specified_return_predicates)
212 else if(statement==ID_fence)
217 throw "unexpected statement: "+
id2string(statement);
const irep_idt & get_statement() const
The type of an expression.
const typet & follow(const typet &src) const
const std::string & id2string(const irep_idt &d)
virtual void symex_assign(statet &state, const code_assignt &code)
goto_programt::const_targett pc
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
virtual void symex_printf(statet &state, const exprt &lhs, const exprt &rhs)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Expression classes for byte-level operators.
Operator to dereference a pointer.
API to expression classes.
irep_idt byte_extract_id()
virtual void symex_input(statet &state, const codet &code)
virtual void symex_other(const goto_functionst &goto_functions, statet &state)
array constructor from single element
bitvector_typet index_type()
void clean_expr(exprt &expr, statet &state, bool write)
Base class for all expressions.
const codet & to_code(const exprt &expr)
void process_array_expr(exprt &expr)
virtual void symex_cpp_delete(statet &state, const codet &code)
A statement in a programming language.
const typet & subtype() const
virtual void symex_output(statet &state, const codet &code)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
virtual void memory_barrier(const exprt &guard, const sourcet &source)=0
symex_targett::sourcet source