28 if(array_op_type.
id()==ID_array)
47 for(std::size_t i=0; i<width; i++)
54 if(array.
id()==ID_symbol)
65 mp_integer array_size = numeric_cast_v<mp_integer>(array_type.
size());
71 if(maybe_index_value.has_value())
81 #define UNIFORM_ARRAY_HACK 82 #ifdef UNIFORM_ARRAY_HACK 83 bool is_uniform = array.
id() == ID_array_of;
85 if(array.
id() == ID_constant || array.
id() == ID_array)
92 [&array](
const exprt &expr) {
return expr == array.
op0(); });
97 static int uniform_array_counter;
99 const std::string identifier =
CPROVER_PREFIX "internal_uniform_array_" +
114 and_exprt range_condition(lower_bound, upper_bound);
125 #define ACTUAL_ARRAY_HACK 126 #ifdef ACTUAL_ARRAY_HACK 129 if((array.
id()==ID_constant || array.
id()==ID_array) &&
132 #ifdef CONSTANT_ARRAY_HACK 137 static int actual_array_counter;
139 const std::string identifier =
CPROVER_PREFIX "internal_actual_array_" +
148 index_equality.
lhs()=index;
153 #ifdef COMPACT_EQUAL_CONST 158 exprt::operandst::const_iterator it = array.
operands().begin();
167 "this loop iterates over the array, so `it` shouldn't be increased " 168 "past the array's end");
170 value_equality.
rhs()=*it++;
190 const bvt &array_bv =
191 convert_bv(array, numeric_cast_v<std::size_t>(array_size * width));
201 for(std::size_t i=0; i<width; i++)
207 index_equality.
lhs()=index;
209 #ifdef COMPACT_EQUAL_CONST 214 equal_bv.resize(width);
223 for(std::size_t j=0; j<width; j++)
225 bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
238 #ifdef COMPACT_EQUAL_CONST 246 "non-positive array sizes are forbidden in goto programs");
256 for(std::size_t j=0; j<width; j++)
258 literalt l = array_bv[numeric_cast_v<std::size_t>(offset + j)];
315 for(std::size_t i=0; i<width; i++)
316 bv[i] = tmp[numeric_cast_v<std::size_t>(offset + i)];
319 array.
id() == ID_member || array.
id() == ID_index ||
320 array.
id() == ID_byte_extract_big_endian ||
321 array.
id() == ID_byte_extract_little_endian)
327 const auto subtype_bytes_opt =
344 for(std::size_t i=0; i<width; i++)
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
The type of an expression, extends irept.
A base class for relations, i.e., binary predicates.
literalt convert(const exprt &expr) override
exprt simplify_expr(const exprt &src, const namespacet &ns)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
boolbv_widtht boolbv_width
bool is_unbounded_array(const typet &type) const override
typet & type()
Return the type of the expression.
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
#define CHECK_RETURN(CONDITION)
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
virtual literalt new_variable()=0
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
API to expression classes.
void conversion_failed(const exprt &expr, bvt &bv)
Split an expression into a base object and a (byte) offset.
const exprt & size() const
The plus expression Associativity is not specified.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt equality(const exprt &e1, const exprt &e2)
mstreamt & result() const
void record_array_index(const index_exprt &expr)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
const exprt & root_object() const
virtual bool has_set_to() const
Expression to hold a symbol (variable)
virtual literalt lselect(literalt a, literalt b, literalt c)=0
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
std::vector< literalt > bvt
irep_idt byte_extract_id()