Go to the documentation of this file.
23 if(expr.
id()==ID_invalid_pointer)
25 if(operands.size()==1 &&
26 operands[0].type().id()==ID_pointer)
48 else if(expr.
id()==ID_dynamic_object)
50 if(operands.size()==1 &&
51 operands[0].type().id()==ID_pointer)
64 else if(expr.
id()==ID_lt || expr.
id()==ID_le ||
65 expr.
id()==ID_gt || expr.
id()==ID_ge)
67 if(operands.size()==2 &&
68 operands[0].type().id()==ID_pointer &&
69 operands[1].type().id()==ID_pointer)
98 if(expr.
id()==ID_symbol)
103 else if(expr.
id()==ID_label)
108 else if(expr.
id() == ID_null_object)
113 else if(expr.
id()==ID_index)
121 if(array_type.
id()==ID_pointer)
127 else if(array_type.
id()==ID_array ||
128 array_type.
id()==ID_incomplete_array ||
129 array_type.
id()==ID_string_constant)
146 else if(expr.
id()==ID_byte_extract_little_endian ||
147 expr.
id()==ID_byte_extract_big_endian)
161 else if(expr.
id()==ID_member)
164 const exprt &struct_op=member_expr.
op0();
171 if(struct_op_type.
id()==ID_struct)
183 struct_op_type.
id() == ID_union,
184 "member expression should operate on struct or union");
190 else if(expr.
id()==ID_constant ||
191 expr.
id()==ID_string_constant ||
197 else if(expr.
id()==ID_if)
226 if(expr.
id()==ID_symbol)
238 else if(expr.
id()==ID_nondet_symbol)
248 else if(expr.
id()==ID_typecast)
252 const exprt &op = typecast_expr.
op();
255 if(op_type.
id()==ID_pointer)
257 else if(op_type.
id()==ID_signedbv ||
258 op_type.
id()==ID_unsignedbv ||
259 op_type.
id()==ID_bool ||
260 op_type.
id()==ID_c_enum ||
261 op_type.
id()==ID_c_enum_tag)
271 else if(expr.
id()==ID_if)
275 else if(expr.
id()==ID_index)
279 else if(expr.
id()==ID_member)
283 else if(expr.
id()==ID_address_of)
299 else if(expr.
id()==ID_constant)
316 else if(expr.
id()==ID_plus)
329 if(it->type().id()==ID_pointer)
337 if(pointer_sub_type.id()==ID_empty)
354 "there should be exactly one pointer-type operand in a pointer-type sum");
360 if(it->type().id()==ID_pointer)
363 if(it->type().id()!=ID_unsignedbv &&
364 it->type().id()!=ID_signedbv)
382 else if(op.size()<
bits)
392 else if(expr.
id()==ID_minus)
399 minus_expr.
op0().
type().
id() == ID_pointer,
400 "first operand should be of pointer type");
405 minus_expr.
op1().
type().
id() != ID_unsignedbv &&
406 minus_expr.
op1().
type().
id() != ID_signedbv)
420 if(pointer_sub_type.id()==ID_empty)
429 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
430 element_size = *element_size_opt;
437 else if(expr.
id()==ID_lshr ||
442 else if(expr.
id()==ID_bitand ||
443 expr.
id()==ID_bitor ||
444 expr.
id()==ID_bitnot)
448 else if(expr.
id()==ID_concatenation)
452 else if(expr.
id()==ID_byte_extract_little_endian ||
453 expr.
id()==ID_byte_extract_big_endian)
460 expr.
id() != ID_byte_update_little_endian,
461 "byte-wise pointer updates are unsupported");
464 expr.
id() != ID_byte_update_big_endian,
465 "byte-wise pointer updates are unsupported");
473 if(expr.
type().
id()==ID_pointer)
476 if(expr.
id()==ID_minus &&
499 if(pointer_sub_type.
id()==ID_empty)
508 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
509 element_size = *element_size_opt;
512 if(element_size != 1)
521 else if(expr.
id()==ID_pointer_offset &&
538 else if(expr.
id()==ID_object_size &&
548 for(std::size_t i=0; i<width; i++)
559 else if(expr.
id()==ID_pointer_object &&
576 else if(expr.
id()==ID_typecast &&
598 const std::vector<bool> &unknown,
600 const typet &type)
const
602 if(type.
id()!=ID_pointer)
605 std::string value_addr, value_offset, value;
607 for(std::size_t i=0; i<
bits; i++)
610 std::size_t bit_nr=i+offset;
628 value_offset=ch+value_offset;
630 value_addr=ch+value_addr;
637 return value[value.size() - 1 - i] ==
'1';
725 const std::size_t max_objects=std::size_t(1)<<
object_bits;
729 "too many addressed objects: maximum number of objects is set to 2^n=" +
732 "use the `--object-bits n` option to increase the maximum number");
740 if(postponed.
expr.
id()==ID_dynamic_object)
745 std::size_t number=0;
752 const exprt &expr=*it;
762 bvt saved_bv=postponed.
op;
763 saved_bv.erase(saved_bv.begin(), saved_bv.begin()+
offset_bits);
777 else if(postponed.
expr.
id()==ID_object_size)
782 std::size_t number=0;
789 const exprt &expr=*it;
791 if(expr.
id() != ID_symbol)
808 bvt saved_bv=postponed.
op;
809 saved_bv.erase(saved_bv.begin(), saved_bv.begin()+
offset_bits);
832 for(postponed_listt::const_iterator
std::size_t get_null_object() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static exprt conditional_cast(const exprt &expr, const typet &type)
#define PRECONDITION(CONDITION)
const typet & subtype() const
virtual bvt convert_member(const member_exprt &expr)
bool convert_address_of_rec(const exprt &expr, bvt &bv)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
virtual bvt convert_bitvector(const exprt &expr)
Converts an expression into its gate-level representation and returns a vector of literals correspond...
The type of an expression, extends irept.
std::vector< literalt > bvt
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
postponed_listt postponed_list
The trinary if-then-else operator.
const mp_integer string2integer(const std::string &n, unsigned base)
std::size_t add_object(const exprt &expr)
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override
bvt sign_extension(const bvt &bv, std::size_t new_size)
The plus expression Associativity is not specified.
void do_postponed(const postponedt &postponed)
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.
virtual void l_set_to(literalt a, bool value)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
virtual bvt convert_pointer_type(const exprt &expr)
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
virtual literalt land(literalt a, literalt b)=0
#define Forall_literals(it, bv)
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
#define UNREACHABLE
This should be used to mark dead code.
virtual bvt convert_concatenation(const concatenation_exprt &expr)
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
struct configt::bv_encodingt bv_encoding
virtual bvt convert_shift(const binary_exprt &expr)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
bvt add(const bvt &op0, const bvt &op1)
boolbv_widtht boolbv_width
mstreamt & result() const
void conversion_failed(const exprt &expr, bvt &bv)
exprt size_of_expr(const typet &type, const namespacet &ns)
virtual literalt limplies(literalt a, literalt b)=0
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const std::string & id2string(const irep_idt &d)
bvt convert_bitvector(const exprt &expr) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
#define forall_operands(it, expr)
const irep_idt & get_identifier() const
virtual bvt convert_if(const if_exprt &expr)
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
literalt const_literal(bool value)
#define POSTCONDITION(CONDITION)
void post_process() override
pointer_logict pointer_logic
pointer_typet pointer_type(const typet &subtype)
The unary minus expression.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
exprt object_size(const exprt &pointer)
const irep_idt & id() const
std::vector< exprt > operandst
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
void encode(std::size_t object, bvt &bv)
literalt convert(const exprt &expr) override
Extract member of struct or union.
virtual bvt convert_bitwise(const exprt &expr)
bvt build_constant(const mp_integer &i, std::size_t width)
virtual literalt lequal(literalt a, literalt b)=0
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
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.
bool is_dynamic_object(const exprt &expr) const
virtual tvt l_get(literalt a) const =0
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
std::size_t get_invalid_object() const
virtual exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
irep_idt get_component_name() const
bv_pointerst(const namespacet &_ns, propt &_prop)
Operator to return the address of an object.
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Semantic type conversion.
tv_enumt get_value() const
void offset_arithmetic(bvt &bv, const mp_integer &x)
literalt convert_rest(const exprt &expr) override
A constant literal expression.
literalt convert_rest(const exprt &expr) override
void post_process() override
const irep_idt & get_value() const
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
typename data_typet::const_iterator const_iterator
virtual void add_addr(const exprt &expr, bvt &bv)
bvt zero_extension(const bvt &bv, std::size_t new_size)
bvt sub(const bvt &op0, const bvt &op1)
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
#define CHECK_RETURN(CONDITION)