Go to the documentation of this file.
26 const typet &array_op_type = array.
type();
30 if(array_op_type.
id()==ID_array)
56 final_array.
id() == ID_symbol || final_array.
id() == ID_nondet_symbol)
68 for(std::size_t i = 0; i < width; i++)
74 if(array.
id() == ID_symbol || array.
id() == ID_nondet_symbol)
92 auto maybe_index_value = numeric_cast<mp_integer>(index);
93 if(maybe_index_value.has_value())
103 #define UNIFORM_ARRAY_HACK
104 #ifdef UNIFORM_ARRAY_HACK
105 bool is_uniform = array.
id() == ID_array_of;
107 if(array.
id() == ID_constant || array.
id() == ID_array)
109 is_uniform = array.
operands().size() <= 1 ||
113 [&array](
const exprt &expr) {
114 return expr == to_multi_ary_expr(array).op0();
120 static int uniform_array_counter;
122 const std::string identifier =
CPROVER_PREFIX "internal_uniform_array_" +
140 and_exprt range_condition(std::move(lower_bound), std::move(upper_bound));
142 std::move(range_condition), std::move(value_equality));
152 #define ACTUAL_ARRAY_HACK
153 #ifdef ACTUAL_ARRAY_HACK
156 if((array.
id()==ID_constant || array.
id()==ID_array) &&
159 #ifdef CONSTANT_ARRAY_HACK
164 static int actual_array_counter;
166 const std::string identifier =
CPROVER_PREFIX "internal_actual_array_" +
174 #ifdef COMPACT_EQUAL_CONST
179 exprt::operandst::const_iterator it = array.
operands().begin();
185 "this loop iterates over the array, so `it` shouldn't be increased "
186 "past the array's end");
207 const bvt &array_bv =
208 convert_bv(array, numeric_cast_v<std::size_t>(array_size * width));
218 for(std::size_t i=0; i<width; i++)
223 #ifdef COMPACT_EQUAL_CONST
228 equal_bv.resize(width);
234 for(std::size_t j=0; j<width; j++)
236 bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
247 #ifdef COMPACT_EQUAL_CONST
255 "non-positive array sizes are forbidden in goto programs");
264 for(std::size_t j=0; j<width; j++)
266 literalt l = array_bv[numeric_cast_v<std::size_t>(offset + j)];
322 for(std::size_t i=0; i<width; i++)
323 bv[i] = tmp[numeric_cast_v<std::size_t>(offset + i)];
326 array.
id() == ID_member || array.
id() == ID_index ||
327 array.
id() == ID_byte_extract_big_endian ||
328 array.
id() == ID_byte_extract_little_endian)
334 const auto subtype_bytes_opt =
351 for(std::size_t i=0; i<width; i++)
const typet & subtype() const
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
bool is_unbounded_array(const typet &type) const override
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
std::vector< literalt > bvt
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
bool has_byte_operator(const exprt &src)
Split an expression into a base object and a (byte) offset.
The plus expression Associativity is not specified.
virtual literalt new_variable()=0
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
Base class for all expressions.
void l_set_to_true(literalt a)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Expression to hold a symbol (variable)
virtual literalt land(literalt a, literalt b)=0
const exprt & size() const
irep_idt byte_extract_id()
typet & type()
Return the type of the expression.
boolbv_widtht boolbv_width
void conversion_failed(const exprt &expr, bvt &bv)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
bool has_operands() const
Return true if there is at least one operand.
virtual literalt limplies(literalt a, literalt b)=0
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
exprt simplify_expr(exprt src, const namespacet &ns)
const irep_idt & id() const
void record_array_index(const index_exprt &expr)
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
const exprt & root_object() const
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
virtual literalt lequal(literalt a, literalt b)=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.
const irep_idt & get(const irep_namet &name) const
A base class for relations, i.e., binary predicates whose two operands have the same type.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
virtual bool has_set_to() const
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
API to expression classes.
virtual literalt lselect(literalt a, literalt b, literalt c)=0
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.