36 for(std::size_t i=0; i<dest.size(); ++i)
80 dest.push_back(value);
106 if(
cell.second.initialized==
170 for(
const auto &
comp : st.components())
251 for(
const auto &
comp : st.components())
322 for(
const auto &op : expr.
operands())
335 for(std::size_t i=0; i<
tmp.size(); ++i)
336 dest.push_back(
tmp[i]);
361 if(i && i->is_zero())
410 for(
const auto &op : expr.
operands())
423 for(std::size_t i=0; i<
tmp.size(); i++)
424 dest.push_back(
tmp[i]);
447 output.
error() <<
"heap memory allocation not fully implemented "
450 std::stringstream buffer;
467 throw id2string(expr.
id())+
" expects at least two operands";
470 for(
const auto &op : expr.
operands())
481 throw id2string(expr.
id())+
" expects at least two operands";
484 for(
const auto &op : expr.
operands())
496 throw id2string(expr.
id())+
" expects at least two operands";
499 for(
const auto &op : expr.
operands())
524 if(
tmp0.size()==1 &&
tmp1.size()==1)
537 if(
tmp0.size()==1 &&
tmp1.size()==1)
550 if(
tmp0.size()==1 &&
tmp1.size()==1)
563 if(
tmp0.size()==1 &&
tmp1.size()==1)
576 if(
tmp0.size()==1 &&
tmp1.size()==1)
595 if(
tmp0.size()==1 &&
tmp1.size()==1)
619 throw id2string(expr.
id())+
" expects at least one operand";
623 for(
const auto &op : expr.
operands())
627 if(
tmp.size()==1 &&
tmp.front()!=0)
652 return {
tmp1.front()};
659 throw id2string(expr.
id())+
" expects at least one operand";
663 for(
const auto &op : expr.
operands())
667 if(
tmp.size()==1 &&
tmp.front()==0)
681 return {
tmp.front() == 0};
689 for(
const auto &op : expr.
operands())
717 for(
const auto &op : expr.
operands())
754 if(
tmp0.size()==1 &&
tmp1.size()==1)
755 return {
tmp0.front() -
tmp1.front()};
763 if(
tmp0.size()==1 &&
tmp1.size()==1)
764 return {
tmp0.front() /
tmp1.front()};
772 return {-
tmp0.front()};
782 throw "pointer_offset expects a pointer operand";
813 if(address.is_zero())
843 else if(!address.is_zero())
854 "evaluate_address should have returned address == 0");
919 for(
const auto &op : expr.
operands())
922 dest.insert(dest.end(),
tmp.begin(),
tmp.end());
941 for(std::size_t i=0; i<
size_int; ++i)
942 dest.insert(dest.end(),
tmp.begin(),
tmp.end());
956 if(!new_value.empty() && where.size()==1 && !
unbounded_size(subtype))
969 for(std::size_t i=0; i<new_value.size(); ++i)
988 output.
error() <<
"!! failed to evaluate expression: "
990 << expr.
id() <<
"[" << expr.
type().
id() <<
"]"
1005 interpretert::memory_mapt::const_iterator
m_it1=
1009 return m_it1->second;
1013 interpretert::memory_mapt::const_iterator
m_it2=
1017 return m_it2->second;
1028 return tmp0.front();
1038 return base+
tmp1.front();
1053 if(
comp.get_name()==component_name)
1086 if(result.size()==1)
1096 output.
error() <<
"!! failed to evaluate address: "
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool has_operands() const
Return true if there is at least one operand.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_boolean() const
Return whether the expression represents a Boolean.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
void from_integer(const mp_integer &i)
void from_expr(const constant_exprt &expr)
const mp_integer & get_value() const
void set_value(const mp_integer &_v)
An IEEE 754 floating-point value, including specificiation.
static ieee_float_valuet one(const floatbv_typet &)
void from_expr(const constant_exprt &expr)
void unpack(const mp_integer &)
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
The trinary if-then-else operator.
void clear_input_flags()
Clears memoy r/w flag initialization.
exprt get_value(const typet &type, const mp_integer &offset=0, bool use_non_det=false)
retrives the constant value at memory location offset as an object of type type
mp_integer base_address_to_actual_size(const mp_integer &address) const
mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false)
bool byte_offset_to_memory_offset(const typet &source_type, const mp_integer &byte_offset, mp_integer &result)
Supposing the caller has an mp_vector representing a value with type 'source_type',...
goto_functionst::function_mapt::const_iterator function
symbol_exprt address_to_symbol(const mp_integer &address) const
void build_memory_map()
Creates a memory map of all static symbols in the program.
std::vector< mp_integer > mp_vectort
mp_vectort evaluate(const exprt &)
Evaluate an expression.
void allocate(const mp_integer &address, const mp_integer &size)
reserves memory block of size at address
void read(const mp_integer &address, mp_vectort &dest) const
Reads a memory address and loads it into the dest variable.
mp_integer address_to_offset(const mp_integer &address) const
bool count_type_leaves(const typet &source_type, mp_integer &result)
Count the number of leaf subtypes of ty, a leaf type is a type that is not an array or a struct.
mp_integer get_size(const typet &type)
Retrieves the actual size of the provided structured type.
bool unbounded_size(const typet &)
bool memory_offset_to_byte_offset(const typet &source_type, const mp_integer &cell_offset, mp_integer &result)
Similarly to the above, the interpreter's memory objects contain mp_integers that represent variable-...
void read_unbounded(const mp_integer &address, mp_vectort &dest) const
const irep_idt & id() const
mstreamt & warning() const
An expression containing a side effect.
Structure type, corresponds to C style structs.
Expression to hold a symbol (variable)
The type of an expression, extends irept.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
Interpreter for GOTO Programs.
const std::string & id2string(const irep_idt &d)
int __CPROVER_ID java::java io InputStream read
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
mp_integer logic_right_shift(const mp_integer &a, const mp_integer &b, std::size_t true_size)
logic right shift (loads 0 on MSB) bitwise operations only make sense on native objects,...
mp_integer arith_left_shift(const mp_integer &a, const mp_integer &b, std::size_t true_size)
arithmetic left shift bitwise operations only make sense on native objects, hence the largest object ...
mp_integer arith_right_shift(const mp_integer &a, const mp_integer &b, std::size_t true_size)
arithmetic right shift (loads sign on MSB) bitwise operations only make sense on native objects,...
mp_integer rotate_right(const mp_integer &a, const mp_integer &b, std::size_t true_size)
rotates right (MSB=LSB) bitwise operations only make sense on native objects, hence the largest objec...
mp_integer bitwise_and(const mp_integer &a, const mp_integer &b)
bitwise 'and' of two nonnegative integers
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise 'or' of two nonnegative integers
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
bitwise 'xor' of two nonnegative integers
mp_integer rotate_left(const mp_integer &a, const mp_integer &b, std::size_t true_size)
rotate left (LSB=MSB) bitwise operations only make sense on native objects, hence the largest object ...
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
bool is_ssa_expr(const exprt &expr)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
side_effect_exprt & to_side_effect_expr(exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
string_containert & get_string_container()
Get a reference to the global string container.