27 if(array_op_type.
id()==ID_array)
46 for(std::size_t i=0; i<width; i++)
53 if(array.
id()==ID_symbol)
66 throw "failed to convert array size";
79 #define UNIFORM_ARRAY_HACK 80 #ifdef UNIFORM_ARRAY_HACK 81 bool is_uniform =
false;
83 if(array.
id()==ID_array_of)
87 else if(array.
id()==ID_constant || array.
id()==ID_array)
89 bool found_exception =
false;
92 if(*it != array.
op0())
94 found_exception =
true;
105 static int uniform_array_counter;
107 std::string identifier=
108 "__CPROVER_internal_uniform_array_"+
121 if(lower_bound.lhs().is_nil() ||
123 throw "number conversion failed (2)";
125 and_exprt range_condition(lower_bound, upper_bound);
136 #define ACTUAL_ARRAY_HACK 137 #ifdef ACTUAL_ARRAY_HACK 140 if((array.
id()==ID_constant || array.
id()==ID_array) &&
143 #ifdef CONSTANT_ARRAY_HACK 148 static int actual_array_counter;
150 std::string identifier=
151 "__CPROVER_internal_actual_array_"+
160 index_equality.
lhs()=index;
165 #ifdef COMPACT_EQUAL_CONST 170 exprt::operandst::const_iterator it = array.
operands().begin();
177 throw "number conversion failed (1)";
179 assert(it != array.
operands().end());
181 value_equality.
rhs()=*it++;
203 if(array_size*width!=array_bv.size())
204 throw "unexpected array size";
214 for(std::size_t i=0; i<width; i++)
220 index_equality.
lhs()=index;
222 #ifdef COMPACT_EQUAL_CONST 227 equal_bv.resize(width);
234 throw "number conversion failed (1)";
238 for(std::size_t j=0; j<width; j++)
253 #ifdef COMPACT_EQUAL_CONST 259 assert(array_size>0);
269 for(std::size_t j=0; j<width; j++)
328 for(std::size_t i=0; i<width; i++)
332 array.
id() == ID_member || array.
id() == ID_index ||
333 array.
id() == ID_byte_extract_big_endian ||
334 array.
id() == ID_byte_extract_little_endian)
355 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.
A generic base class for relations, i.e., binary predicates.
literalt convert(const exprt &expr) override
exprt simplify_expr(const exprt &src, const namespacet &ns)
boolbv_widtht boolbv_width
bool is_unbounded_array(const typet &type) const override
#define forall_expr(it, expr)
const exprt & root_object() const
#define CHECK_RETURN(CONDITION)
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
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
virtual const bvt & convert_bv(const exprt &expr)
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)
irep_idt byte_extract_id()
split an expression into a base object and a (byte) offset
const exprt & size() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const typet & follow(const typet &) const
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 generic 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
virtual bool has_set_to() const
std::string to_string(const string_constraintt &expr)
Used for debug printing.
Expression to hold a symbol (variable)
virtual literalt lselect(literalt a, literalt b, literalt c)=0
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
std::vector< literalt > bvt