10 #ifndef CPROVER_UTIL_STD_EXPR_H 11 #define CPROVER_UTIL_STD_EXPR_H 27 DEPRECATED(
"use nullary_exprt(id, type) instead")
63 DEPRECATED(
"use ternary_exprt(id, op0, op1, op2, type) instead")
69 DEPRECATED(
"use ternary_exprt(id, op0, op1, op2, type) instead")
118 "Transition systems must have three operands");
119 return static_cast<const transt &
>(expr);
128 "Transition systems must have three operands");
129 return static_cast<transt &
>(expr);
134 return base.id()==ID_trans;
146 DEPRECATED(
"use symbol_exprt(identifier, type) instead")
152 DEPRECATED(
"use symbol_exprt(identifier, type) instead")
173 set(ID_identifier, identifier);
178 return get(ID_identifier);
187 DEPRECATED(
"use decorated_symbol_exprt(identifier, type) instead")
193 DEPRECATED(
"use decorated_symbol_exprt(identifier, type) instead")
200 DEPRECATED(
"use decorated_symbol_exprt(identifier, type) instead")
216 return get_bool(ID_C_static_lifetime);
221 return set(ID_C_static_lifetime,
true);
226 remove(ID_C_static_lifetime);
236 return set(ID_C_thread_local,
true);
241 remove(ID_C_thread_local);
268 return base.id()==ID_symbol;
290 set(ID_identifier, identifier);
295 return get(ID_identifier);
322 return base.id()==ID_nondet_symbol;
354 DEPRECATED(
"use unary_exprt(id, op, type) instead")
399 "Unary expressions must have one operand");
408 "Unary expressions must have one operand");
414 return base.operands().size()==1;
444 "Absolute value must have one operand");
445 return static_cast<const abs_exprt &
>(expr);
454 "Absolute value must have one operand");
460 return base.id()==ID_abs;
472 DEPRECATED(
"use unary_minus_exprt(op) instead")
501 "Unary minus must have one operand");
511 "Unary minus must have one operand");
517 return base.id()==ID_unary_minus;
544 expr.
operands().size() == 1,
"unary plus must have one operand");
553 expr.
operands().size() == 1,
"unary plus must have one operand");
560 return base.id() == ID_unary_plus;
590 set(ID_bits_per_byte, bits_per_byte);
605 expr.
op0().
type() == expr.
type(),
"bswap type must match operand type");
615 expr.
op0().
type() == expr.
type(),
"bswap type must match operand type");
622 return base.id() == ID_bswap;
628 value.
op().
type() == value.
type(),
"bswap type must match operand type");
646 DEPRECATED(
"use unary_predicate_exprt(id, op) instead")
654 DEPRECATED(
"use binary_predicate_exprt(op1, id, op2) instead")
669 DEPRECATED(
"use unary_predicate_exprt(id, op) instead")
674 DEPRECATED(
"use unary_predicate_exprt(id, op) instead")
714 expr.
operands().size() == 1,
"sign expression must have one operand");
723 expr.
operands().size() == 1,
"sign expression must have one operand");
730 return base.id() == ID_sign;
741 DEPRECATED(
"use binary_exprt(lhs, id, rhs) instead")
747 DEPRECATED(
"use binary_exprt(lhs, id, rhs) instead")
753 DEPRECATED(
"use binary_exprt(lhs, id, rhs, type) instead")
787 "binary expression must have two operands");
814 "Binary expressions must have two operands");
823 "Binary expressions must have two operands");
829 return base.operands().size()==2;
838 DEPRECATED(
"use binary_predicate_exprt(lhs, id, rhs) instead")
843 DEPRECATED(
"use binary_predicate_exprt(lhs, id, rhs) instead")
872 expr.
type().
id() == ID_bool,
873 "result of binary predicate expression should be of type bool");
881 DEPRECATED(
"use binary_relation_exprt(lhs, id, rhs) instead")
886 DEPRECATED(
"use binary_relation_exprt(lhs, id, rhs) instead")
918 "lhs and rhs of binary relation expression should have same type");
952 "Binary relations must have two operands");
961 "Binary relations must have two operands");
976 DEPRECATED(
"use multi_ary_exprt(id, op, type) instead")
981 DEPRECATED(
"use multi_ary_exprt(id, op, type) instead")
986 DEPRECATED(
"use multi_ary_exprt(id, op, type) instead")
1015 const typet &_type):
1045 DEPRECATED(
"use plus_exprt(lhs, rhs) instead")
1064 const typet &_type):
1081 "Plus must have two or more operands");
1082 return static_cast<const plus_exprt &
>(expr);
1091 "Plus must have two or more operands");
1097 return base.id()==ID_plus;
1109 DEPRECATED(
"use minus_exprt(lhs, rhs) instead")
1133 "Minus must have two or more operands");
1143 "Minus must have two or more operands");
1149 return base.id()==ID_minus;
1162 DEPRECATED(
"use mult_exprt(lhs, rhs) instead")
1186 "Multiply must have two or more operands");
1187 return static_cast<const mult_exprt &
>(expr);
1196 "Multiply must have two or more operands");
1202 return base.id()==ID_mult;
1214 DEPRECATED(
"use div_exprt(lhs, rhs) instead")
1262 "Divide must have two operands");
1263 return static_cast<const div_exprt &
>(expr);
1272 "Divide must have two operands");
1278 return base.id()==ID_div;
1290 DEPRECATED(
"use mod_exprt(lhs, rhs) instead")
1313 return static_cast<const mod_exprt &
>(expr);
1326 return base.id()==ID_mod;
1338 DEPRECATED(
"use rem_exprt(lhs, rhs) instead")
1361 return static_cast<const rem_exprt &
>(expr);
1374 return base.id()==ID_rem;
1386 DEPRECATED(
"use power_exprt(lhs, rhs) instead")
1422 return base.id()==ID_power;
1434 DEPRECATED(
"use factorial_power_exprt(lhs, rhs) instead")
1458 "Factorial power must have two operands");
1468 "Factorial power must have two operands");
1475 return base.id()==ID_factorial_power;
1487 DEPRECATED(
"use equal_exprt(lhs, rhs) instead")
1536 return base.id()==ID_equal;
1548 DEPRECATED(
"use notequal_exprt(lhs, rhs) instead")
1570 "Inequality must have two operands");
1580 "Inequality must have two operands");
1586 return base.id()==ID_notequal;
1598 DEPRECATED(
"use index_exprt(array, index) instead")
1603 DEPRECATED(
"use index_exprt(array, index) instead")
1614 const exprt &_array,
1615 const exprt &_index,
1616 const typet &_type):
1653 "Array index must have two operands");
1663 "Array index must have two operands");
1669 return base.id()==ID_index;
1681 DEPRECATED(
"use array_of_exprt(what, type) instead")
1714 "'Array of' must have one operand");
1724 "'Array of' must have one operand");
1730 return base.id()==ID_array_of;
1774 return base.id()==ID_array;
1791 return base.id() == ID_array_list;
1835 return base.id()==ID_vector;
1843 DEPRECATED(
"use union_exprt(component_name, value, type) instead")
1848 DEPRECATED(
"use union_exprt(component_name, value, type) instead")
1856 const exprt &_value,
1865 return get(ID_component_name);
1870 set(ID_component_name, component_name);
1880 set(ID_component_number, component_number);
1895 "Union constructor must have one operand");
1905 "Union constructor must have one operand");
1911 return base.id()==ID_union;
1923 DEPRECATED(
"use struct_exprt(component_name, value, type) instead")
1957 return base.id()==ID_struct;
1965 DEPRECATED(
"use complex_exprt(r, i, type) instead")
1970 DEPRECATED(
"use complex_exprt(r, i, type) instead")
2016 "Complex constructor must have two operands");
2026 "Complex constructor must have two operands");
2032 return base.id()==ID_complex;
2060 "real part retrieval operation must have one operand");
2070 "real part retrieval operation must have one operand");
2077 return base.id() == ID_complex_real;
2083 expr, 1,
"real part retrieval operation must have one operand");
2107 "imaginary part retrieval operation must have one operand");
2117 "imaginary part retrieval operation must have one operand");
2124 return base.id() == ID_complex_imag;
2130 expr, 1,
"imaginary part retrieval operation must have one operand");
2141 op0().
id(ID_unknown);
2142 op1().
id(ID_unknown);
2182 "Object descriptor must have two operands");
2192 "Object descriptor must have two operands");
2199 return base.id()==ID_object_descriptor;
2213 op0().
id(ID_unknown);
2214 op1().
id(ID_unknown);
2220 op0().
id(ID_unknown);
2221 op1().
id(ID_unknown);
2251 "Dynamic object must have two operands");
2261 "Dynamic object must have two operands");
2267 return base.id()==ID_dynamic_object;
2280 DEPRECATED(
"use typecast_exprt(op, type) instead")
2311 "Typecast must have one operand");
2321 "Typecast must have one operand");
2327 return base.id()==ID_typecast;
2339 DEPRECATED(
"use floatbv_typecast_exprt(op, r, type) instead")
2346 const exprt &rounding,
2383 "Float typecast must have two operands");
2393 "Float typecast must have two operands");
2400 return base.id()==ID_floatbv_typecast;
2461 return static_cast<const and_exprt &
>(expr);
2476 return base.id()==ID_and;
2488 DEPRECATED(
"use implies_exprt(a, b) instead")
2522 return base.id()==ID_implies;
2583 return static_cast<const or_exprt &
>(expr);
2593 return static_cast<or_exprt &
>(expr);
2598 return base.id()==ID_or;
2629 return static_cast<const xor_exprt &
>(expr);
2641 return base.id()==ID_xor;
2693 return base.id()==ID_bitnot;
2705 DEPRECATED(
"use bitor_exprt(op0, op1) instead")
2744 return base.id()==ID_bitor;
2760 DEPRECATED(
"use bitxor_exprt(op0, op1) instead")
2798 return base.id()==ID_bitxor;
2814 DEPRECATED(
"use bitand_exprt(op0, op1) instead")
2853 return base.id()==ID_bitand;
2869 DEPRECATED(
"use shift_exprt(value, id, distance) instead")
2874 DEPRECATED(
"use shift_exprt(value, id, distance) instead")
2888 const std::size_t _distance);
2921 "Shifts must have two operands");
2930 "Shifts must have two operands");
2947 DEPRECATED(
"use shl_exprt(value, distance) instead")
2967 DEPRECATED(
"use ashl_exprt(value, distance) instead")
2987 DEPRECATED(
"use lshl_exprt(value, distance) instead")
3007 DEPRECATED(
"use replication_exprt(times, value) instead")
3012 DEPRECATED(
"use replication_exprt(times, value) instead")
3055 "Bit-wise replication must have two operands");
3065 "Bit-wise replication must have two operands");
3071 return base.id()==ID_replication;
3083 DEPRECATED(
"use extractbit_exprt(value, index) instead")
3098 const std::size_t _index);
3132 "Extract bit must have two operands");
3142 "Extract bit must have two operands");
3148 return base.id()==ID_extractbit;
3160 DEPRECATED(
"use extractbits_exprt(value, upper, lower) instead")
3173 const exprt &_upper,
3174 const exprt &_lower,
3175 const typet &_type):
exprt(ID_extractbits, _type)
3184 const std::size_t _upper,
3185 const std::size_t _lower,
3186 const typet &_type);
3230 "Extract bits must have three operands");
3240 "Extract bits must have three operands");
3246 return base.id()==ID_extractbits;
3299 return base.id()==ID_address_of;
3332 return static_cast<const not_exprt &
>(expr);
3345 return base.id()==ID_not;
3358 DEPRECATED(
"use dereference_exprt(pointer) instead")
3363 DEPRECATED(
"use dereference_exprt(pointer) instead")
3402 "Dereference must have one operand");
3412 "Dereference must have one operand");
3418 return base.id()==ID_dereference;
3440 DEPRECATED(
"use if_exprt(cond, t, f) instead")
3487 "If-then-else must have three operands");
3488 return static_cast<const if_exprt &
>(expr);
3497 "If-then-else must have three operands");
3498 return static_cast<if_exprt &
>(expr);
3503 return base.id()==ID_if;
3519 const exprt &_where,
3520 const exprt &_new_value):
3526 DEPRECATED(
"use with_exprt(old, where, new_value) instead")
3574 "Array/structure update must have three operands");
3575 return static_cast<const with_exprt &
>(expr);
3584 "Array/structure update must have three operands");
3590 return base.id()==ID_with;
3597 "Array/structure update must have three operands");
3605 exprt(ID_index_designator)
3632 "Index designator must have one operand");
3642 "Index designator must have one operand");
3648 return base.id()==ID_index_designator;
3660 exprt(ID_member_designator)
3662 set(ID_component_name, _component_name);
3667 return get(ID_component_name);
3682 "Member designator must not have operands");
3692 "Member designator must not have operands");
3698 return base.id()==ID_member_designator;
3712 const exprt &_designator,
3713 const exprt &_new_value)
3718 DEPRECATED(
"use update_exprt(old, where, new_value) instead")
3723 DEPRECATED(
"use update_exprt(old, where, new_value) instead")
3726 op1().
id(ID_designator);
3775 "Array/structure update must have three operands");
3785 "Array/structure update must have three operands");
3791 return base.id()==ID_update;
3798 "Array/structure update must have three operands");
3803 class array_update_exprt:
public exprt 3808 const exprt &_array,
3809 const exprt &_index,
3810 const exprt &_new_value):
3811 exprt(ID_array_update, _array.type())
3816 array_update_exprt():
exprt(ID_array_update)
3826 const exprt &array()
const 3836 const exprt &index()
const 3846 const exprt &new_value()
const 3858 inline const array_update_exprt &to_array_update_expr(
const exprt &expr)
3863 "Array update must have three operands");
3864 return static_cast<const array_update_exprt &
>(expr);
3868 inline array_update_exprt &to_array_update_expr(
exprt &expr)
3873 "Array update must have three operands");
3874 return static_cast<array_update_exprt &
>(expr);
3877 template<>
inline bool can_cast_expr<array_update_exprt>(
const exprt &base)
3879 return base.id()==ID_array_update;
3896 const typet &_type):
3910 DEPRECATED(
"use member_exprt(op, c) instead")
3917 return get(ID_component_name);
3922 set(ID_component_name, component_name);
3964 "Extract member must have one operand");
3974 "Extract member must have one operand");
3980 return base.id()==ID_member;
4026 return base.id()==ID_isnan;
4060 "Is infinite must have one operand");
4070 "Is infinite must have one operand");
4076 return base.id()==ID_isinf;
4122 return base.id()==ID_isfinite;
4168 return base.id()==ID_isnormal;
4180 DEPRECATED(
"use ieee_float_equal_exprt(lhs, rhs) instead")
4202 "IEEE equality must have two operands");
4212 "IEEE equality must have two operands");
4219 return base.id()==ID_ieee_float_equal;
4231 DEPRECATED(
"use ieee_float_notequal_exprt(lhs, rhs) instead")
4255 "IEEE inequality must have two operands");
4265 "IEEE inequality must have two operands");
4272 return base.id()==ID_ieee_float_notequal;
4285 DEPRECATED(
"use ieee_float_op_exprt(lhs, id, rhs, rm) instead")
4342 "IEEE float operations must have three arguments");
4351 "IEEE float operations must have three arguments");
4387 DEPRECATED(
"use constant_exprt(value, type) instead")
4392 DEPRECATED(
"use constant_exprt(value, type) instead")
4398 exprt(ID_constant, _type)
4405 return get(ID_value);
4410 set(ID_value, value);
4438 return base.id()==ID_constant;
4492 function()=_function;
4529 "Function application must have two operands");
4539 "Function application must have two operands");
4546 return base.id()==ID_function_application;
4561 DEPRECATED(
"use concatenation_exprt(op, type) instead")
4566 DEPRECATED(
"use concatenation_exprt(op, type) instead")
4610 return base.id()==ID_concatenation;
4687 return static_cast<const let_exprt &
>(expr);
4700 return base.id()==ID_let;
4714 const exprt &_where)
4749 "quantifier expressions must have two operands");
4751 expr.
op0().
id() == ID_symbol,
"quantified variable shall be a symbol");
4759 "quantifier expressions must have two operands");
4761 expr.
op0().
id() == ID_symbol,
"quantified variable shall be a symbol");
4767 return base.id() == ID_forall || base.id() == ID_exists;
4773 "quantifier expressions must have two operands");
4801 "exists expressions have exactly two operands");
4810 "exists expressions have exactly two operands");
4818 DEPRECATED(
"use popcount_exprt(op, type) instead")
4858 return base.id() == ID_popcount;
4897 expr.
operands().size() % 2 != 0,
"cond must have even number of operands");
4898 return static_cast<const cond_exprt &
>(expr);
4906 expr.
operands().size() % 2 != 0,
"cond must have even number of operands");
4910 #endif // CPROVER_UTIL_STD_EXPR_H const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
bool can_cast_expr< rem_exprt >(const exprt &base)
const irept & get_nil_irep()
exprt & component(const irep_idt &name, const namespacet &ns)
const transt & to_trans_expr(const exprt &expr)
Cast an exprt to a transt expr must be known to be transt.
const ieee_float_equal_exprt & to_ieee_float_equal_expr(const exprt &expr)
Cast an exprt to an ieee_float_equal_exprt.
const irep_idt & get_name() const
bitnot_exprt(const exprt &op)
bool can_cast_expr< update_exprt >(const exprt &base)
bool can_cast_expr< bitxor_exprt >(const exprt &base)
The type of an expression, extends irept.
bool can_cast_expr< implies_exprt >(const exprt &base)
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const typet &_type)
bool can_cast_expr< isnormal_exprt >(const exprt &base)
const factorial_power_exprt & to_factorial_power_expr(const exprt &expr)
Cast an exprt to a factorial_power_exprt.
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
unary_minus_exprt(const exprt &_op, const typet &_type)
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Semantic type conversion.
or_exprt(const exprt &op0, const exprt &op1)
const exprt & rhs() const
bool can_cast_expr< mult_exprt >(const exprt &base)
bool can_cast_expr< quantifier_exprt >(const exprt &base)
An expression without operands.
bool can_cast_expr< bitnot_exprt >(const exprt &base)
function_application_exprt(const symbol_exprt &_function, const argumentst &_arguments, const typet &_type)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
A base class for relations, i.e., binary predicates.
cond_exprt(const typet &_type)
const exprt & value() const
if_exprt(const exprt &cond, const exprt &t, const exprt &f, const typet &type)
const exprt & lhs() const
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Application of (mathematical) function.
void set_identifier(const irep_idt &identifier)
forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
bool can_cast_expr< typecast_exprt >(const exprt &base)
index_exprt(const exprt &_array, const exprt &_index)
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
ieee_float_notequal_exprt(const exprt &_lhs, const exprt &_rhs)
bool can_cast_expr< transt >(const exprt &base)
binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const typet &_type)
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
let_exprt(const symbol_exprt &symbol, const exprt &value, const exprt &where)
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Operator to update elements in structs and arrays.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
bool can_cast_expr< concatenation_exprt >(const exprt &base)
const exprt & pointer() const
Evaluates to true if the operand is infinite.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
address_of_exprt(const exprt &op)
bool can_cast_expr< with_exprt >(const exprt &base)
and_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
unsigned int get_instance() const
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
const exprt & real() const
const exprt & array() const
bswap_exprt(const exprt &_op, std::size_t bits_per_byte, const typet &_type)
bool can_cast_expr< array_of_exprt >(const exprt &base)
const irep_idt & get_identifier() const
or_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
exprt::operandst & designator()
shift_exprt(const irep_idt &_id)
const exprt & op3() const =delete
ternary_exprt(const irep_idt &_id, const exprt &_op0, const exprt &_op1, const exprt &_op2, const typet &_type)
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
const irep_idt & get_value() const
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
The null pointer constant.
An expression denoting a type.
abs_exprt(const exprt &_op)
bool can_cast_expr< member_designatort >(const exprt &base)
type_exprt(const typet &type)
concatenation_exprt(operandst &&_operands, const typet &_type)
plus_exprt(const exprt &_lhs, const exprt &_rhs, const typet &_type)
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
const exprt & op1() const =delete
Transition system, consisting of state invariant, initial state predicate, and transition predicate...
bool is_thread_local() const
The trinary if-then-else operator.
std::size_t get_component_number() const
const exists_exprt & to_exists_expr(const exprt &expr)
Evaluates to true if the operand is a normal number.
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
multi_ary_exprt(const irep_idt &_id, operandst &&_operands, const typet &_type)
typet & type()
Return the type of the expression.
const symbol_exprt & symbol() const
bool can_cast_expr< factorial_power_exprt >(const exprt &base)
bool can_cast_expr< extractbit_exprt >(const exprt &base)
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
bool can_cast_expr< bitand_exprt >(const exprt &base)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const exprt & op2() const =delete
const exprt & where() const
bool can_cast_expr< array_list_exprt >(const exprt &base)
const exprt & where() const
A constant literal expression.
bool can_cast_expr< mod_exprt >(const exprt &base)
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
bool can_cast_expr< and_exprt >(const exprt &base)
const exprt & dividend() const
The dividend of a division is the number that is being divided.
bool get_bool(const irep_namet &name) const
bool can_cast_expr< index_designatort >(const exprt &base)
const exprt & index() const
const exprt & op3() const =delete
symbol_exprt(const typet &type)
const exprt & where() const
irep_idt get_component_name() const
bool value_is_zero_string() const
Imaginary part of the expression describing a complex number.
bool can_cast_expr< sign_exprt >(const exprt &base)
void set_bits_per_byte(std::size_t bits_per_byte)
const ieee_float_notequal_exprt & to_ieee_float_notequal_expr(const exprt &expr)
Cast an exprt to an ieee_float_notequal_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
void set_component_number(std::size_t component_number)
ieee_float_op_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const exprt &_rm)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
or_exprt(const exprt &op0, const exprt &op1, const exprt &op2, const exprt &op3)
vector_exprt(const vector_typet &_type)
bool can_cast_expr< ieee_float_equal_exprt >(const exprt &base)
Extract member of struct or union.
const exprt & imag() const
const exprt & rounding_mode() const
bool can_cast_expr< not_exprt >(const exprt &base)
void set_instance(unsigned int instance)
Concatenation of bit-vector operands.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
bool can_cast_expr< bitor_exprt >(const exprt &base)
bool can_cast_expr< plus_exprt >(const exprt &base)
bool can_cast_expr< div_exprt >(const exprt &base)
Templated functions to cast to specific exprt-derived classes.
constant_exprt(const irep_idt &_value, const typet &_type)
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
void set_component_name(const irep_idt &component_name)
bool can_cast_expr< function_application_exprt >(const exprt &base)
binary_predicate_exprt(const exprt &_op0, const irep_idt &_id, const exprt &_op1)
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
exprt conjunction(const exprt::operandst &)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const exprt & compound() const
binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
bswap_exprt(const exprt &_op, std::size_t bits_per_byte)
if_exprt(const exprt &cond, const exprt &t, const exprt &f)
const irep_idt & id() const
dereference_exprt(const exprt &op, const typet &type)
popcount_exprt(const exprt &_op)
const exprt & op2() const =delete
The unary plus expression.
void set_value(const irep_idt &value)
const exprt & times() const
Evaluates to true if the operand is NaN.
bool can_cast_expr< isnan_exprt >(const exprt &base)
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
An expression denoting infinity.
shift_exprt(const exprt &_src, const irep_idt &_id, const exprt &_distance)
bool can_cast_expr< minus_exprt >(const exprt &base)
The Boolean constant true.
unary_exprt(const irep_idt &_id, const exprt &_op, const typet &_type)
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
binary_relation_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
A base class for binary expressions.
const exprt & invar() const
decorated_symbol_exprt(const irep_idt &identifier, const typet &type)
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const exprt & distance() const
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const irep_idt & get_identifier() const
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Real part of the expression describing a complex number.
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
unary_minus_exprt(const exprt &_op)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
IEEE floating-point disequality.
bool can_cast_expr< member_exprt >(const exprt &base)
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
member_exprt(const exprt &op, const struct_typet::componentt &c)
bool can_cast_expr< vector_exprt >(const exprt &base)
const exprt & op3() const =delete
const exprt & op1() const =delete
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Operator to dereference a pointer.
operandst & operands()=delete
remove all operand methods
const exprt & op0() const =delete
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
bool can_cast_expr< complex_exprt >(const exprt &base)
Union constructor from single element.
std::size_t get_component_number() const
factorial_power_exprt(const exprt &_base, const exprt &_exp)
bool can_cast_expr< binary_exprt >(const exprt &base)
const exprt & new_value() const
popcount_exprt(const exprt &_op, const typet &_type)
not_exprt(const exprt &op)
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const exprt & lhs() const
and_exprt(const exprt &op0, const exprt &op1)
Generic base class for unary expressions.
exprt::operandst argumentst
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
infinity_exprt(const typet &_type)
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
An expression with three operands.
bool can_cast_expr< union_exprt >(const exprt &base)
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const exprt & what() const
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
unary_exprt(const irep_idt &_id, const exprt &_op)
#define PRECONDITION(CONDITION)
const exprt & false_case() const
typecast_exprt(const typet &_type)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
bool can_cast_expr< extractbits_exprt >(const exprt &base)
lshr_exprt(const exprt &_src, const std::size_t _distance)
Split an expression into a base object and a (byte) offset.
const exprt & cond() const
with_exprt(const exprt &_old, const exprt &_where, const exprt &_new_value)
The plus expression Associativity is not specified.
bool can_cast_expr< constant_exprt >(const exprt &base)
symbol_exprt(const irep_idt &identifier, const typet &type)
const symbol_exprt & symbol() const
bool can_cast_expr< floatbv_typecast_exprt >(const exprt &base)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
null_pointer_exprt(const pointer_typet &type)
ieee_float_equal_exprt(const exprt &_lhs, const exprt &_rhs)
void set_static_lifetime()
Array constructor from single element.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
bool can_cast_expr< xor_exprt >(const exprt &base)
exprt disjunction(const exprt::operandst &)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
bool can_cast_expr< abs_exprt >(const exprt &base)
power_exprt(const exprt &_base, const exprt &_exp)
isfinite_exprt(const exprt &op)
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Vector constructor from list of elements.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
const exprt & old() const
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
bool can_cast_expr< or_exprt >(const exprt &base)
bool can_cast_expr< dereference_exprt >(const exprt &base)
Operator to return the address of an object.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
The unary minus expression.
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
concatenation_exprt(const exprt &_op0, const exprt &_op1, const typet &_type)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
implies_exprt(const exprt &op0, const exprt &op1)
predicate_exprt(const irep_idt &_id)
union_exprt(const irep_idt &_component_name, const exprt &_value, const typet &_type)
member_exprt(const exprt &op, const irep_idt &component_name, const typet &_type)
quantifier_exprt(const irep_idt &_id, const symbol_exprt &_symbol, const exprt &_where)
bool has_operands() const
Return true if there is at least one operand.
const exprt & index() const
bool can_cast_expr< address_of_exprt >(const exprt &base)
The Boolean constant false.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const exprt & init() const
bool can_cast_expr< replication_exprt >(const exprt &base)
const exprt & rhs() const
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
equal_exprt(const exprt &_lhs, const exprt &_rhs)
void validate_expr(const transt &value)
const exprt & trans() const
static exprt conditional_cast(const exprt &expr, const typet &type)
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
std::vector< exprt > operandst
Binary multiplication Associativity is not specified.
const exprt::operandst & designator() const
bool can_cast_expr< ieee_float_notequal_exprt >(const exprt &base)
bool can_cast_expr< notequal_exprt >(const exprt &base)
void clear_thread_local()
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const exprt & object() const
const power_exprt & to_power_expr(const exprt &expr)
Cast an exprt to a power_exprt.
minus_exprt(const exprt &_lhs, const exprt &_rhs)
index_designatort(const exprt &_index)
Complex numbers made of pair of given subtype.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
bool can_cast_expr< symbol_exprt >(const exprt &base)
dynamic_object_exprt(const typet &type)
complex_imag_exprt(const exprt &op)
const exprt & op3() const =delete
typecast_exprt(const exprt &op, const typet &_type)
const exprt & old() const
const exprt & object() const
plus_exprt(const typet &type)
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
plus_exprt(const exprt &_lhs, const exprt &_rhs)
update_exprt(const exprt &_old, const exprt &_designator, const exprt &_new_value)
Expression to hold a nondeterministic choice.
bitand_exprt(const exprt &_op0, const exprt &_op1)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
shl_exprt(const exprt &_src, const exprt &_distance)
The popcount (counting the number of bits set to 1) expression.
const rem_exprt & to_rem_expr(const exprt &expr)
Cast an exprt to a rem_exprt.
Evaluates to true if the operand is finite.
ashr_exprt(const exprt &_src, const exprt &_distance)
std::size_t get_bits_per_byte() const
xor_exprt(const exprt &_op0, const exprt &_op1)
Semantic type conversion from/to floating-point formats.
div_exprt(const exprt &_lhs, const exprt &_rhs)
object_descriptor_exprt()
shl_exprt(const exprt &_src, const std::size_t _distance)
Base class for all expressions.
Sign of an expression Predicate is true if _op is negative, false otherwise.
const exprt & root_object() const
floatbv_typecast_exprt(const exprt &op, const exprt &rounding, const typet &_type)
const exprt & struct_op() const
const exprt & rounding_mode() const
isnormal_exprt(const exprt &op)
nondet_symbol_exprt(const irep_idt &identifier, const typet &type)
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
dereference_exprt(const exprt &op)
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
complex_real_exprt(const exprt &op)
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const exprt & op2() const =delete
factorial_power_exprt & to_factorial_expr(exprt &expr)
Cast an exprt to a factorial_power_exprt.
Operator to update elements in structs and arrays.
sign_exprt(const exprt &_op)
A base class for quantifier expressions.
lshr_exprt(const exprt &_src, const exprt &_distance)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
unary_predicate_exprt(const irep_idt &_id, const exprt &_op)
irep_idt get_component_name() const
const exprt & offset() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bool can_cast_expr< let_exprt >(const exprt &base)
rem_exprt(const exprt &_lhs, const exprt &_rhs)
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const exprt & valid() const
bitor_exprt(const exprt &_op0, const exprt &_op1)
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const exprt & true_case() const
void set_identifier(const irep_idt &identifier)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs, expressions, instructions, etc.
array_exprt(const array_typet &_type)
irep_idt get_component_name() const
bool can_cast_expr< unary_exprt >(const exprt &base)
void set_component_name(const irep_idt &component_name)
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
and_exprt(const exprt &op0, const exprt &op1, const exprt &op2, const exprt &op3)
bool is_static_lifetime() const
isinf_exprt(const exprt &op)
bool can_cast_expr< bswap_exprt >(const exprt &base)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
isnan_exprt(const exprt &op)
Expression to hold a symbol (variable)
bool can_cast_expr< isinf_exprt >(const exprt &base)
bool can_cast_expr< power_exprt >(const exprt &base)
ashr_exprt(const exprt &_src, const std::size_t _distance)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
bool can_cast_expr< isfinite_exprt >(const exprt &base)
bool can_cast_expr< struct_exprt >(const exprt &base)
replication_exprt(const exprt &_times, const exprt &_src)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
struct_exprt(const typet &_type)
bool can_cast_expr< index_exprt >(const exprt &base)
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
void clear_static_lifetime()
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
exprt & dividend()
The dividend of a division is the number that is being divided.
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
Representation of heap-allocated objects.
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
A base class for multi-ary expressions Associativity is not specified.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
mult_exprt(const exprt &_lhs, const exprt &_rhs)
mod_exprt(const exprt &_lhs, const exprt &_rhs)
void copy_to_operands(const exprt &expr)=delete
bitxor_exprt(const exprt &_op0, const exprt &_op1)
Bit-wise negation of bit-vectors.
index_exprt(const exprt &_array, const exprt &_index, const typet &_type)
Struct constructor from list of elements.
unary_plus_exprt(const exprt &op)
bool can_cast_expr< if_exprt >(const exprt &base)
std::size_t get_size_t(const irep_namet &name) const
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
notequal_exprt(const exprt &_lhs, const exprt &_rhs)
complex_exprt(const exprt &_real, const exprt &_imag, const complex_typet &_type)
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
void move_to_operands(exprt &)=delete
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
array_list_exprt(const array_typet &_type)
A base class for shift operators.
const argumentst & arguments() const
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Array constructor from list of elements.
nullary_exprt(const irep_idt &_id, const typet &_type)
Complex constructor from a pair of numbers.
bool can_cast_expr< array_exprt >(const exprt &base)
The byte swap expression.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
member_designatort(const irep_idt &_component_name)
bool can_cast_expr< popcount_exprt >(const exprt &base)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Array constructor from a list of index-element pairs Operands are index/value pairs, alternating.
array_of_exprt(const exprt &_what, const array_typet &_type)
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
A base class for expressions that are predicates, i.e., Boolean-typed.
IEEE-floating-point equality.
bool can_cast_expr< equal_exprt >(const exprt &base)
address_of_exprt(const exprt &op, const pointer_typet &_type)
const exprt & new_value() const