Go to the documentation of this file.
10 #ifndef CPROVER_UTIL_STD_EXPR_H
11 #define CPROVER_UTIL_STD_EXPR_H
67 {std::move(_op0), std::move(_op1), std::move(_op2)})
108 set(ID_identifier, identifier);
113 return get(ID_identifier);
131 return get_bool(ID_C_static_lifetime);
136 return set(ID_C_static_lifetime,
true);
141 remove(ID_C_static_lifetime);
151 return set(ID_C_thread_local,
true);
156 remove(ID_C_thread_local);
163 return base.
id() == ID_symbol;
222 set(ID_identifier, identifier);
227 return get(ID_identifier);
234 return base.
id() == ID_nondet_symbol;
344 return base.
id() == ID_abs;
381 :
unary_exprt(ID_unary_minus, std::move(_op), std::move(_type))
394 return base.
id() == ID_unary_minus;
438 return base.
id() == ID_unary_plus;
474 :
unary_exprt(ID_bswap, std::move(_op), std::move(_type))
492 set(ID_bits_per_byte, narrow_cast<long long>(bits_per_byte));
499 return base.
id() == ID_bswap;
506 value.
op().
type() == value.
type(),
"bswap type must match operand type");
568 return base.
id() == ID_sign;
609 :
expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
620 "binary expression must have two operands");
717 expr.
type().
id() == ID_bool,
718 "result of binary predicate expression should be of type bool");
752 expr_binary.op0().type() == expr_binary.op1().type(),
753 "lhs and rhs of binary relation expression should have same type");
805 :
expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
906 return base.
id() == ID_plus;
943 :
binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
951 return base.
id() == ID_minus;
997 return base.
id() == ID_mult;
1034 :
binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
1066 return base.
id() == ID_div;
1103 :
binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1111 return base.
id() == ID_mod;
1148 :
binary_exprt(std::move(_lhs), ID_rem, std::move(_rhs))
1156 return base.
id() == ID_rem;
1216 return base.
id() == ID_equal;
1259 return base.
id() == ID_notequal;
1296 :
binary_exprt(_array, ID_index, std::move(_index), _array.
type().subtype())
1333 return base.
id() == ID_index;
1370 :
unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1398 return base.
id() == ID_array_of;
1453 return base.
id() == ID_array;
1481 :
multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1505 return base.
id() == ID_array_list;
1542 return base.
id() == ID_vector;
1570 :
unary_exprt(ID_union, std::move(_value), std::move(_type))
1577 return get(ID_component_name);
1582 set(ID_component_name, component_name);
1592 set(ID_component_number, narrow_cast<long long>(component_number));
1599 return base.
id() == ID_union;
1647 return base.
id() == ID_struct;
1707 return base.
id() == ID_complex;
1751 return base.
id() == ID_complex_real;
1757 expr, 1,
"real part retrieval operation must have one operand");
1796 return base.
id() == ID_complex_imag;
1802 expr, 1,
"imaginary part retrieval operation must have one operand");
1837 ID_object_descriptor,
1846 ID_object_descriptor,
1884 return base.
id() == ID_object_descriptor;
1949 return base.
id() == ID_dynamic_object;
1997 expr.
operands().size() == 1,
"is_dynamic_object must have one operand");
2007 expr.
operands().size() == 1,
"is_dynamic_object must have one operand");
2033 return base.
id() == ID_typecast;
2072 ID_floatbv_typecast,
2073 std::move(rounding),
2102 return base.
id() == ID_floatbv_typecast;
2147 {std::move(
op0), std::move(
op1), std::move(
op2)},
2155 {std::move(
op0), std::move(
op1), std::move(
op2), std::move(
op3)},
2175 return base.
id() == ID_and;
2187 return static_cast<const and_exprt &
>(expr);
2211 return base.
id() == ID_implies;
2255 {std::move(
op0), std::move(
op1), std::move(
op2)},
2263 {std::move(
op0), std::move(
op1), std::move(
op2), std::move(
op3)},
2283 return base.
id() == ID_or;
2295 return static_cast<const or_exprt &
>(expr);
2302 return static_cast<or_exprt &
>(expr);
2319 return base.
id() == ID_xor;
2331 return static_cast<const xor_exprt &
>(expr);
2354 return base.
id() == ID_bitnot;
2399 return base.
id() == ID_bitor;
2435 return base.
id() == ID_bitxor;
2471 return base.
id() == ID_bitand;
2499 :
binary_exprt(std::move(_src), _id, std::move(_distance))
2529 return base.
id() == ID_shl || base.
id() == ID_ashr || base.
id() == ID_lshr;
2564 :
shift_exprt(std::move(_src), ID_shl, std::move(_distance))
2602 :
shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
2607 :
shift_exprt(std::move(_src), ID_ashr, _distance)
2617 :
shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
2622 :
shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
2663 return base.
id() == ID_extractbit;
2708 {std::move(_src), std::move(_upper), std::move(_lower)})
2714 const std::size_t _upper,
2715 const std::size_t _lower,
2752 return base.
id() == ID_extractbits;
2791 :
unary_exprt(ID_address_of, std::move(
op), std::move(_type))
2809 return base.
id() == ID_address_of;
2854 return base.
id() == ID_not;
2918 "dereference expression must have one operand");
2930 return base.
id() == ID_dereference;
3015 return base.
id() == ID_if;
3056 {_old, std::move(_where), std::move(_new_value)})
3094 return base.
id() == ID_with;
3100 value, 3,
"array/structure update must have at least 3 operands",
true);
3103 "array/structure update must have an odd number of operands");
3151 return base.
id() == ID_index_designator;
3188 set(ID_component_name, _component_name);
3193 return get(ID_component_name);
3200 return base.
id() == ID_member_designator;
3240 std::move(_designator),
3241 std::move(_new_value),
3284 return base.
id() == ID_update;
3290 value, 3,
"Array/structure update must have three operands");
3323 const exprt &_array,
3324 const exprt &_index,
3325 const exprt &_new_value):
3326 exprt(ID_array_update, _array.type())
3341 const exprt &array()
const
3351 const exprt &index()
const
3361 const exprt &new_value()
const
3367 template<>
inline bool can_cast_expr<array_update_exprt>(
const exprt &base)
3369 return base.
id()==ID_array_update;
3383 inline const array_update_exprt &to_array_update_expr(
const exprt &expr)
3386 const array_update_exprt &ret =
static_cast<const array_update_exprt &
>(expr);
3392 inline array_update_exprt &to_array_update_expr(
exprt &expr)
3395 array_update_exprt &ret =
static_cast<array_update_exprt &
>(expr);
3421 return get(ID_component_name);
3426 set(ID_component_name, component_name);
3463 "member expression must have one operand");
3475 return base.
id() == ID_member;
3520 return base.
id() == ID_isnan;
3565 return base.
id() == ID_isinf;
3610 return base.
id() == ID_isfinite;
3655 return base.
id() == ID_isnormal;
3694 ID_ieee_float_equal,
3703 return base.
id() == ID_ieee_float_equal;
3743 ID_ieee_float_notequal,
3752 return base.
id() == ID_ieee_float_notequal;
3835 return base.
id() == ID_floatbv_plus || base.
id() == ID_floatbv_minus ||
3836 base.
id() == ID_floatbv_div || base.
id() == ID_floatbv_mult;
3842 value, 3,
"IEEE float operations must have three arguments");
3880 return base.
id() == ID_type;
3916 return get(ID_value);
3921 set(ID_value, value);
3930 return base.
id() == ID_constant;
3984 return base.
id() == ID_nil;
4030 return base.
id() == ID_replication;
4070 :
multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
4077 {std::move(_op0), std::move(_op1)},
4086 return base.
id() == ID_concatenation;
4275 return base.
id() == ID_let;
4311 :
unary_exprt(ID_popcount, std::move(_op), std::move(_type))
4324 return base.
id() == ID_popcount;
4381 return base.
id() == ID_cond;
4387 value.
operands().size() % 2 == 0,
"cond must have even number of operands");
4430 ID_array_comprehension,
4470 return base.
id() == ID_array_comprehension;
4535 set(ID_identifier, std::move(
id));
4547 return get(ID_component_name);
4555 return get(ID_C_class);
4562 return get(ID_C_base_name);
4570 return get(ID_identifier);
4579 "class method descriptor must have a mangled method name.");
4581 !value.
class_id().
empty(),
"class method descriptor must have a class id.");
4584 "class method descriptor must have a base method name.");
4588 "class method descriptor must have an identifier in the expected format.");
4610 return base.
id() == ID_virtual_function;
4613 #endif // CPROVER_UTIL_STD_EXPR_H
Operator to update elements in structs and arrays.
const exprt & array() const
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
dynamic_object_exprt(typet type)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
if_exprt(exprt cond, const exprt &t, exprt f)
bool can_cast_expr< symbol_exprt >(const exprt &base)
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
bool can_cast_expr< union_exprt >(const exprt &base)
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
static exprt conditional_cast(const exprt &expr, const typet &type)
bool can_cast_expr< rem_exprt >(const exprt &base)
const exprt & index() const
shl_exprt(exprt _src, const std::size_t _distance)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
bool can_cast_expr< isnan_exprt >(const exprt &base)
A base class for multi-ary expressions Associativity is not specified.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
bool can_cast_expr< cond_exprt >(const exprt &base)
member_exprt(exprt op, const irep_idt &component_name, typet _type)
bool can_cast_expr< array_list_exprt >(const exprt &base)
bool can_cast_expr< mod_exprt >(const exprt &base)
const exprt & where() const
if_exprt(exprt cond, exprt t, exprt f, typet type)
member_designatort(const irep_idt &_component_name)
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
bool can_cast_expr< index_designatort >(const exprt &base)
bool can_cast_expr< isinf_exprt >(const exprt &base)
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
array_list_exprt(operandst _operands, array_typet _type)
const operandst & operands() const =delete
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Expression to hold a nondeterministic choice.
and_exprt(exprt::operandst _operands)
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 can_cast_expr< complex_imag_exprt >(const exprt &base)
lshr_exprt(exprt _src, exprt _distance)
bool can_cast_expr< concatenation_exprt >(const exprt &base)
void copy_to_operands(const exprt &, const exprt &)=delete
const irep_idt & get_identifier() const
const exprt & rhs() const
bool can_cast_expr< floatbv_typecast_exprt >(const exprt &base)
std::size_t size() const
Amount of nodes this expression tree contains.
const exprt & real() const
unary_minus_exprt(exprt _op, typet _type)
const type_exprt & to_type_expr(const exprt &expr)
Cast an exprt to an type_exprt.
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
bool can_cast_expr< bitor_exprt >(const exprt &base)
bool can_cast_expr< not_exprt >(const exprt &base)
The type of an expression, extends irept.
ieee_float_notequal_exprt(exprt _lhs, exprt _rhs)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
An expression with three operands.
mult_exprt(exprt _lhs, exprt _rhs)
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.
bool can_cast_expr< sign_exprt >(const exprt &base)
ieee_float_equal_exprt(exprt _lhs, exprt _rhs)
Operator to dereference a pointer.
Representation of heap-allocated objects.
bool can_cast_expr< unary_exprt >(const exprt &base)
const exprt & true_case() const
The trinary if-then-else operator.
Evaluates to true if the operand is a pointer to a dynamic object.
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
bool can_cast_expr< isfinite_exprt >(const exprt &base)
div_exprt(exprt _lhs, exprt _rhs)
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Split an expression into a base object and a (byte) offset.
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the dereference expression has the right number of operands, refers to something with a po...
plus_exprt(exprt _lhs, exprt _rhs)
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Real part of the expression describing a complex number.
address_of_exprt(const exprt &op)
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Union constructor from single element.
exprt disjunction(const exprt::operandst &)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
bitxor_exprt(exprt _op0, exprt _op1)
bool can_cast_expr< bitxor_exprt >(const exprt &base)
const ieee_float_equal_exprt & to_ieee_float_equal_expr(const exprt &expr)
Cast an exprt to an ieee_float_equal_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
bool can_cast_expr< ieee_float_notequal_exprt >(const exprt &base)
The plus expression Associativity is not specified.
bool can_cast_expr< xor_exprt >(const exprt &base)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Base class for all expressions.
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
const exprt & op1() const =delete
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Generic base class for unary expressions.
ashr_exprt(exprt _src, exprt _distance)
array_exprt(operandst _operands, array_typet _type)
dereference_exprt(const exprt &op)
index_exprt(exprt _array, exprt _index, typet _type)
void clear_static_lifetime()
A base class for binary expressions.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
bswap_exprt(exprt _op, std::size_t bits_per_byte)
irep_idt get_component_name() const
Complex numbers made of pair of given subtype.
std::size_t get_bits_per_byte() const
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Sign of an expression Predicate is true if _op is negative, false otherwise.
bool can_cast_expr< binary_exprt >(const exprt &base)
const exprt::operandst & designator() const
const array_typet & type() const
predicate_exprt(const irep_idt &_id)
const exprt & old() const
static void validate(const exprt &, validation_modet)
const symbol_exprt & arg() const
cond_exprt(operandst _operands, typet _type)
bool can_cast_expr< minus_exprt >(const exprt &base)
const array_list_exprt & to_array_list_expr(const exprt &expr)
Concatenation of bit-vector operands.
index_designatort(exprt _index)
void copy_to_operands(const exprt &, const exprt &, const exprt &)=delete
void move_to_operands(exprt &)=delete
Vector constructor from list of elements.
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
index_exprt(const exprt &_array, exprt _index)
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
bool can_cast_expr< bitand_exprt >(const exprt &base)
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
Expression to hold a symbol (variable)
bool can_cast_expr< array_exprt >(const exprt &base)
void validate_expr(const symbol_exprt &value)
bool can_cast_expr< member_exprt >(const exprt &base)
minus_exprt(exprt _lhs, exprt _rhs)
std::size_t get_component_number() const
const array_typet & type() const
const rem_exprt & to_rem_expr(const exprt &expr)
Cast an exprt to a rem_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const exprt & rounding_mode() const
bool can_cast_expr< equal_exprt >(const exprt &base)
An expression denoting infinity.
void add(exprt index, exprt value)
add an index/value pair
Evaluates to true if the operand is finite.
bool can_cast_expr< implies_exprt >(const exprt &base)
const exprt & op3() const =delete
void set_component_name(const irep_idt &component_name)
const exprt & op3() const =delete
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
An expression describing a method on a class.
Struct constructor from list of elements.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
IEEE floating-point disequality.
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
const irep_idt & get_identifier() const
A unique identifier of the combination of class and method overload to which this expression refers.
typet & type()
Return the type of the expression.
exprt & value()
convenience accessor for the value of a single binding
or_exprt(exprt::operandst _operands)
An expression without operands.
bool get_bool(const irep_namet &name) const
bool can_cast_expr< let_exprt >(const exprt &base)
bool can_cast_expr< bitnot_exprt >(const exprt &base)
bool can_cast_expr< and_exprt >(const exprt &base)
std::size_t get_component_number() const
const array_typet & type() const
const exprt & where() const
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
and_exprt(exprt op0, exprt op1, exprt op2)
unsigned int get_instance() const
address_of_exprt(exprt op, pointer_typet _type)
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
xor_exprt(exprt _op0, exprt _op1)
rem_exprt(exprt _lhs, exprt _rhs)
notequal_exprt(exprt _lhs, exprt _rhs)
void move_to_operands(exprt &, exprt &, exprt &)=delete
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
const exprt & value() const
convenience accessor for the value of a single binding
const exprt & pointer() const
bool can_cast_expr< abs_exprt >(const exprt &base)
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
complex_real_exprt(const exprt &op)
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
and_exprt(exprt op0, exprt op1)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const irep_idt & base_method_name() const
The name of the method to which this expression is applied as would be seen in the source code.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
The null pointer constant.
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
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)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
void set_static_lifetime()
const irep_idt & get_name() const
symbol_exprt(const irep_idt &identifier, typet type)
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
Semantic type conversion from/to floating-point formats.
const exprt & compound() const
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
A base class for expressions that are predicates, i.e., Boolean-typed.
bitor_exprt(const exprt &_op0, exprt _op1)
const exprt & op1() const
bool can_cast_expr< address_of_exprt >(const exprt &base)
bool can_cast_expr< plus_exprt >(const exprt &base)
const exprt & new_value() const
const exprt & struct_op() const
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
#define PRECONDITION(CONDITION)
operandst & operands()=delete
remove all operand methods
bool can_cast_expr< array_of_exprt >(const exprt &base)
const irep_idt & get_identifier() const
dereference_exprt(exprt op, typet type)
Array constructor from single element.
void set_identifier(const irep_idt &identifier)
const exprt & index() const
exprt conjunction(const exprt::operandst &)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
shl_exprt(exprt _src, exprt _distance)
bool is_thread_local() const
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
bool can_cast_expr< bswap_exprt >(const exprt &base)
floatbv_typecast_exprt(exprt op, exprt rounding, typet _type)
bool can_cast_expr< notequal_exprt >(const exprt &base)
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
bool can_cast_expr< nil_exprt >(const exprt &base)
bool can_cast_expr< ieee_float_op_exprt >(const exprt &base)
const exprt & body() const
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
null_pointer_exprt(pointer_typet type)
const exprt & valid() const
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Binary multiplication Associativity is not specified.
std::vector< symbol_exprt > variablest
const exprt & old() const
concatenation_exprt(operandst _operands, typet _type)
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
is_dynamic_object_exprt(const exprt &op)
mod_exprt(exprt _lhs, exprt _rhs)
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
The unary minus expression.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const exprt & op3() const =delete
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const variablest & variables() const
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
struct_exprt(operandst _operands, typet _type)
const exprt & rounding_mode() const
const irep_idt & id() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const binding_exprt & binding() const
void remove(const irep_namet &name)
A base class for variable bindings (quantifiers, let, lambda)
popcount_exprt(const exprt &_op)
bool can_cast_expr< div_exprt >(const exprt &base)
std::vector< exprt > operandst
Complex constructor from a pair of numbers.
The Boolean constant false.
const operandst & values() const
vector_exprt(operandst _operands, vector_typet _type)
The unary plus expression.
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
const exprt & cond() const
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
const exprt & object() const
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
const exprt & dividend() const
The dividend of a division is the number that is being divided.
const exprt & root_object() const
const exprt & imag() const
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const ieee_float_notequal_exprt & to_ieee_float_notequal_expr(const exprt &expr)
Cast an exprt to an ieee_float_notequal_exprt.
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
const array_typet & type() const
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
exprt & dividend()
The dividend of a division is the number that is being divided.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Operator to update elements in structs and arrays.
const exprt & op0() const =delete
bool can_cast_expr< extractbit_exprt >(const exprt &base)
exprt::operandst & designator()
object_descriptor_exprt(exprt _object)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
const exprt & op0() const
unary_plus_exprt(exprt op)
bool can_cast_expr< replication_exprt >(const exprt &base)
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
bool can_cast_expr< index_exprt >(const exprt &base)
unary_exprt(const irep_idt &_id, const exprt &_op)
irep_idt get_component_name() const
Bit-wise negation of bit-vectors.
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
unary_minus_exprt(exprt _op)
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
Extract member of struct or union.
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
equal_exprt(exprt _lhs, exprt _rhs)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
A base class for shift operators.
void set_instance(unsigned int instance)
bool can_cast_expr< complex_real_exprt >(const exprt &base)
An expression denoting a type.
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
plus_exprt(operandst _operands, typet _type)
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
infinity_exprt(typet _type)
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
const exprt & offset() const
std::size_t get_size_t(const irep_namet &name) const
bool can_cast_expr< or_exprt >(const exprt &base)
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
void copy_to_operands(const exprt &expr)=delete
decorated_symbol_exprt(const irep_idt &identifier, typet type)
bitand_exprt(const exprt &_op0, exprt _op1)
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const irep_idt & get(const irep_namet &name) const
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
Evaluates to true if the operand is infinite.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr)
Cast an exprt to a class_method_descriptor_exprt.
bool value_is_zero_string() const
replication_exprt(const constant_exprt &_times, const exprt &_src)
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
const exprt & lhs() const
member_exprt(exprt op, const struct_typet::componentt &c)
const exprt & op2() const =delete
bool can_cast_expr< type_exprt >(const exprt &base)
void set(const irep_namet &name, const irep_idt &value)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bool can_cast_expr< popcount_exprt >(const exprt &base)
const exprt & false_case() const
lshr_exprt(exprt _src, const std::size_t _distance)
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
A base class for relations, i.e., binary predicates whose two operands have the same type.
typecast_exprt(exprt op, typet _type)
Templated functions to cast to specific exprt-derived classes.
const exprt & op1() const =delete
Imaginary part of the expression describing a complex number.
bool can_cast_expr< shift_exprt >(const exprt &base)
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
nullary_exprt(const irep_idt &_id, typet _type)
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
const exprt & lhs() const
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
void clear_thread_local()
bool can_cast_expr< isnormal_exprt >(const exprt &base)
void set_bits_per_byte(std::size_t bits_per_byte)
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const irep_idt & class_id() const
Unique identifier in the symbol table, of the compile time type of the class which this expression is...
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
or_exprt(exprt op0, exprt op1, exprt op2)
const exprt & op2() const
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
concatenation_exprt(exprt _op0, exprt _op1, typet _type)
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
bool can_cast_expr< typecast_exprt >(const exprt &base)
The byte swap expression.
const exprt & distance() const
bool can_cast_expr< vector_exprt >(const exprt &base)
irep_idt get_component_name() const
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
const irept & get_nil_irep()
const exprt & where() const
convenience accessor for binding().where()
bool can_cast_expr< if_exprt >(const exprt &base)
const exprt & what() const
exprt & component(const irep_idt &name, const namespacet &ns)
Array constructor from a list of index-element pairs Operands are index/value pairs,...
constant_exprt(const irep_idt &_value, typet _type)
bool can_cast_expr< constant_exprt >(const exprt &base)
bool is_static_lifetime() const
bool can_cast_expr< complex_exprt >(const exprt &base)
or_exprt(exprt op0, exprt op1)
ashr_exprt(exprt _src, const std::size_t _distance)
const exprt & op2() const =delete
const exprt & rhs() const
Operator to return the address of an object.
source_locationt & add_source_location()
The popcount (counting the number of bits set to 1) expression.
object_descriptor_exprt()
const exprt & object() const
Semantic type conversion.
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
unary_predicate_exprt(const irep_idt &_id, exprt _op)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
complex_imag_exprt(const exprt &op)
Expression to define a mapping from an argument (index) to elements.
const constant_exprt & times() const
The Boolean constant true.
A constant literal expression.
bool can_cast_expr< extractbits_exprt >(const exprt &base)
IEEE-floating-point equality.
const exprt & op2() const =delete
const exprt & op3() const =delete
implies_exprt(exprt op0, exprt op1)
bool can_cast_expr< struct_exprt >(const exprt &base)
bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
exprt & where()
convenience accessor for binding().where()
binding_exprt & binding()
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
void set_component_number(std::size_t component_number)
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
void set_value(const irep_idt &value)
const irep_idt & get_value() const
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
array_of_exprt(exprt _what, array_typet _type)
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Array constructor from list of elements.
bool can_cast_expr< with_exprt >(const exprt &base)
Evaluates to true if the operand is a normal number.
void set_component_name(const irep_idt &component_name)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
popcount_exprt(exprt _op, typet _type)
void set_identifier(const irep_idt &identifier)
const exprt & new_value() const
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
ieee_float_op_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs, exprt _rm)
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Base class for all expressions.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
bool can_cast_expr< member_designatort >(const exprt &base)
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
bool can_cast_expr< update_exprt >(const exprt &base)
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
bool can_cast_expr< dereference_exprt >(const exprt &base)
bool can_cast_expr< ieee_float_equal_exprt >(const exprt &base)
Evaluates to true if the operand is NaN.
void move_to_operands(exprt &, exprt &)=delete
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
bool can_cast_expr< mult_exprt >(const exprt &base)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
nondet_symbol_exprt(const irep_idt &identifier, typet type)
const exprt & op3() const