23 std::vector<mp_integer> &dest)
const 43 std::vector<mp_integer> &dest)
const 45 if(expr.
id()==ID_constant)
47 if(expr.
type().
id()==ID_struct)
50 else if(expr.
type().
id()==ID_floatbv)
54 dest.push_back(f.
pack());
57 else if(expr.
type().
id()==ID_fixedbv)
64 else if(expr.
type().
id()==ID_bool)
79 else if(expr.
id()==ID_struct)
86 if(it->type().id()==ID_code)
89 unsigned sub_size=
get_size(it->type());
93 std::vector<mp_integer> tmp;
96 if(tmp.size()==sub_size)
98 for(
unsigned i=0; i<sub_size; i++)
99 dest.push_back(tmp[i]);
110 else if(expr.
id()==ID_equal ||
111 expr.
id()==ID_notequal ||
118 throw id2string(expr.
id())+
" expects two operands";
120 std::vector<mp_integer> tmp0, tmp1;
124 if(tmp0.size()==1 && tmp1.size()==1)
129 if(expr.
id()==ID_equal)
130 dest.push_back(op0==op1);
131 else if(expr.
id()==ID_notequal)
132 dest.push_back(op0!=op1);
133 else if(expr.
id()==ID_le)
134 dest.push_back(op0<=op1);
135 else if(expr.
id()==ID_ge)
136 dest.push_back(op0>=op1);
137 else if(expr.
id()==ID_lt)
138 dest.push_back(op0<op1);
139 else if(expr.
id()==ID_gt)
140 dest.push_back(op0>op1);
145 else if(expr.
id()==ID_or)
148 throw id2string(expr.
id())+
" expects at least one operand";
154 std::vector<mp_integer> tmp;
157 if(tmp.size()==1 && tmp.front()!=0)
164 dest.push_back(result);
168 else if(expr.
id()==ID_if)
171 throw "if expects three operands";
173 std::vector<mp_integer> tmp0, tmp1, tmp2;
178 if(tmp0.size()==1 && tmp1.size()==1 && tmp2.size()==1)
184 dest.push_back(op0!=0?op1:op2);
189 else if(expr.
id()==ID_and)
192 throw id2string(expr.
id())+
" expects at least one operand";
198 std::vector<mp_integer> tmp;
201 if(tmp.size()==1 && tmp.front()==0)
208 dest.push_back(result);
212 else if(expr.
id()==ID_not)
217 std::vector<mp_integer> tmp;
221 dest.push_back(tmp.front()==0);
225 else if(expr.
id()==ID_plus)
231 std::vector<mp_integer> tmp;
237 dest.push_back(result);
240 else if(expr.
id()==ID_mult)
245 if(expr.
type().
id()==ID_fixedbv)
252 else if(expr.
type().
id()==ID_floatbv)
263 std::vector<mp_integer> tmp;
267 if(expr.
type().
id()==ID_fixedbv)
277 else if(expr.
type().
id()==ID_floatbv)
291 dest.push_back(result);
294 else if(expr.
id()==ID_minus)
297 throw "- expects two operands";
299 std::vector<mp_integer> tmp0, tmp1;
303 if(tmp0.size()==1 && tmp1.size()==1)
304 dest.push_back(tmp0.front()-tmp1.front());
307 else if(expr.
id()==ID_div)
310 throw "/ expects two operands";
312 std::vector<mp_integer> tmp0, tmp1;
316 if(tmp0.size()==1 && tmp1.size()==1)
317 dest.push_back(tmp0.front()/tmp1.front());
320 else if(expr.
id()==ID_unary_minus)
323 throw "unary- expects one operand";
325 std::vector<mp_integer> tmp0;
329 dest.push_back(-tmp0.front());
332 else if(expr.
id()==ID_address_of)
335 throw "address_of expects one operand";
340 else if(expr.
id()==ID_dereference ||
341 expr.
id()==ID_index ||
342 expr.
id()==ID_symbol ||
343 expr.
id()==ID_member)
350 else if(expr.
id()==ID_typecast)
353 throw "typecast expects one operand";
355 std::vector<mp_integer> tmp;
362 if(expr.
type().
id()==ID_pointer)
364 dest.push_back(value);
367 else if(expr.
type().
id()==ID_signedbv)
374 else if(expr.
type().
id()==ID_unsignedbv)
381 else if(expr.
type().
id()==ID_bool)
383 dest.push_back(value!=0);
388 else if(expr.
id()==ID_ashr)
391 throw "ashr expects two operands";
393 std::vector<mp_integer> tmp0, tmp1;
397 if(tmp0.size()==1 && tmp1.size()==1)
398 dest.push_back(tmp0.front()/
power(2, tmp1.front()));
403 std::cout <<
"!! failed to evaluate expression: " 410 if(expr.
id()==ID_symbol)
412 const irep_idt &identifier=expr.
get(ID_identifier);
414 interpretert::memory_mapt::const_iterator m_it1=
418 return m_it1->second;
422 interpretert::memory_mapt::const_iterator m_it2=
426 return m_it2->second;
429 else if(expr.
id()==ID_dereference)
432 throw "dereference expects one operand";
434 std::vector<mp_integer> tmp0;
440 else if(expr.
id()==ID_index)
443 throw "index expects two operands";
445 std::vector<mp_integer> tmp1;
451 else if(expr.
id()==ID_member)
454 throw "member expects one operand";
464 for(
const auto &comp : struct_type.
components())
466 if(comp.get_name()==component_name)
475 std::cout <<
"!! failed to evaluate address: " const typet & follow(const typet &src) const
const std::string & id2string(const irep_idt &d)
void set_value(const mp_integer &_v)
void from_expr(const constant_exprt &expr)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
void from_expr(const constant_exprt &expr)
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
void read(mp_integer address, std::vector< mp_integer > &dest) const
const componentst & components() const
void evaluate(const exprt &expr, std::vector< mp_integer > &dest) const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
const mp_integer & get_value() const
const irep_idt & id() const
Interpreter for GOTO Programs.
void unpack(const mp_integer &i)
goto_functionst::function_mapt::const_iterator function
void from_integer(const mp_integer &i)
API to expression classes.
const irep_idt & get(const irep_namet &name) const
#define forall_operands(it, expr)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
unsigned get_size(const typet &type) const
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Base class for all expressions.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
irep_idt get_component_name() const
const std::string integer2binary(const mp_integer &n, std::size_t width)
mp_integer evaluate_address(const exprt &expr) const
void from_integer(const mp_integer &i)
std::size_t integer2size_t(const mp_integer &n)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.