10 #ifndef CPROVER_UTIL_STD_EXPR_H 11 #define CPROVER_UTIL_STD_EXPR_H 64 "Transition systems must have three operands");
65 return static_cast<const transt &
>(expr);
76 "Transition systems must have three operands");
77 return static_cast<transt &
>(expr);
117 set(ID_identifier, identifier);
122 return get(ID_identifier);
163 return get_bool(ID_C_static_lifetime);
168 return set(ID_C_static_lifetime,
true);
173 remove(ID_C_static_lifetime);
183 return set(ID_C_thread_local,
true);
188 remove(ID_C_thread_local);
283 "Unary expressions must have one operand");
294 "Unary expressions must have one operand");
328 "Absolute value must have one operand");
329 return static_cast<const abs_exprt &
>(expr);
340 "Absolute value must have one operand");
381 "Unary minus must have one operand");
393 "Unary minus must have one operand");
528 "Binary expressions must have two operands");
539 "Binary expressions must have two operands");
623 "Binary relations must have two operands");
634 "Binary relations must have two operands");
740 "Plus must have two or more operands");
752 "Plus must have two or more operands");
788 "Minus must have two or more operands");
800 "Minus must have two or more operands");
836 "Multiply must have two or more operands");
848 "Multiply must have two or more operands");
884 "Divide must have two operands");
885 return static_cast<const div_exprt &
>(expr);
896 "Divide must have two operands");
931 return static_cast<const mod_exprt &
>(expr);
975 return static_cast<const rem_exprt &
>(expr);
1064 "Factorial power must have two operands");
1076 "Factorial power must have two operands");
1152 "Inequality must have two operands");
1164 "Inequality must have two operands");
1184 exprt(ID_index, _array.
type().subtype())
1190 const exprt &_array,
1191 const exprt &_index,
1192 const typet &_type):
1193 exprt(ID_index, _type)
1234 "Array index must have two operands");
1246 "Array index must have two operands");
1291 "'Array of' must have one operand");
1303 "'Array of' must have one operand");
1317 exprt(ID_array, _type)
1357 exprt(ID_vector, _type)
1403 const exprt &_value,
1404 const typet &_type):
1412 return get(ID_component_name);
1417 set(ID_component_name, component_name);
1427 set(ID_component_number, component_number);
1446 "Union constructor must have one operand");
1458 "Union constructor must have one operand");
1472 exprt(ID_struct, _type)
1558 "Complex constructor must have two operands");
1570 "Complex constructor must have two operands");
1584 op0().
id(ID_unknown);
1585 op1().
id(ID_unknown);
1604 while(p->
id()==ID_member || p->
id()==ID_index)
1640 "Object descriptor must have two operands");
1652 "Object descriptor must have two operands");
1664 op0().
id(ID_unknown);
1665 op1().
id(ID_unknown);
1672 op0().
id(ID_unknown);
1673 op1().
id(ID_unknown);
1707 "Dynamic object must have two operands");
1719 "Dynamic object must have two operands");
1734 exprt(ID_typecast, _type)
1765 "Typecast must have one operand");
1777 "Typecast must have one operand");
1792 const exprt &rounding,
1834 "Float typecast must have two operands");
1846 "Float typecast must have two operands");
1909 return static_cast<const and_exprt &
>(expr);
2025 return static_cast<const or_exprt &
>(expr);
2037 return static_cast<or_exprt &
>(expr);
2247 const std::size_t _distance);
2284 "Shifts must have two operands");
2295 "Shifts must have two operands");
2416 "Bit-wise replication must have two operands");
2428 "Bit-wise replication must have two operands");
2449 const std::size_t _index);
2487 "Extract bit must have two operands");
2499 "Extract bit must have two operands");
2516 const exprt &_upper,
2517 const exprt &_lower,
2518 const typet &_type):
exprt(ID_extractbits, _type)
2525 const std::size_t _upper,
2526 const std::size_t _lower,
2527 const typet &_type);
2575 "Extract bits must have three operands");
2587 "Extract bits must have three operands");
2686 return static_cast<const not_exprt &
>(expr);
2711 exprt(ID_dereference)
2753 "Dereference must have one operand");
2765 "Dereference must have one operand");
2841 "If-then-else must have three operands");
2842 return static_cast<const if_exprt &
>(expr);
2853 "If-then-else must have three operands");
2854 return static_cast<if_exprt &
>(expr);
2866 const exprt &_where,
2867 const exprt &_new_value):
2924 "Array/structure update must have three operands");
2925 return static_cast<const with_exprt &
>(expr);
2936 "Array/structure update must have three operands");
2944 exprt(ID_index_designator)
2975 "Index designator must have one operand");
2987 "Index designator must have one operand");
2995 exprt(ID_member_designator)
2997 set(ID_component_name, _component_name);
3002 return get(ID_component_name);
3021 "Member designator must not have operands");
3033 "Member designator must not have operands");
3044 const exprt &_designator,
3045 const exprt &_new_value):
3052 exprt(ID_update, _type)
3060 op1().
id(ID_designator);
3113 "Array/structure update must have three operands");
3125 "Array/structure update must have three operands");
3132 class array_update_exprt:
public exprt 3136 const exprt &_array,
3137 const exprt &_index,
3138 const exprt &_new_value):
3139 exprt(ID_array_update, _array.type())
3144 array_update_exprt():
exprt(ID_array_update)
3154 const exprt &array()
const 3164 const exprt &index()
const 3174 const exprt &new_value()
const 3190 inline const array_update_exprt &to_array_update_expr(
const exprt &expr)
3195 "Array update must have three operands");
3196 return static_cast<const array_update_exprt &
>(expr);
3202 inline array_update_exprt &to_array_update_expr(
exprt &expr)
3207 "Array update must have three operands");
3208 return static_cast<array_update_exprt &
>(expr);
3237 const typet &_type):
3238 exprt(ID_member, _type)
3251 return get(ID_component_name);
3256 set(ID_component_name, component_name);
3266 set(ID_component_number, component_number);
3307 "Extract member must have one operand");
3319 "Extract member must have one operand");
3395 "Is infinite must have one operand");
3407 "Is infinite must have one operand");
3525 "IEEE equality must have two operands");
3537 "IEEE equality must have two operands");
3573 "IEEE inequality must have two operands");
3585 "IEEE inequality must have two operands");
3654 "IEEE float operations must have three arguments");
3665 "IEEE float operations must have three arguments");
3697 exprt(ID_constant, _type)
3704 return get(ID_value);
3709 set(ID_value, value);
3832 "Function application must have two operands");
3844 "Function application must have two operands");
3863 exprt(ID_concatenation, _type)
3869 exprt(ID_concatenation, _type)
3912 exprt(ID_infinity, _type)
3973 return static_cast<const let_exprt &
>(expr);
4050 #endif // CPROVER_UTIL_STD_EXPR_H const abs_exprt & to_abs_expr(const exprt &expr)
Cast a generic exprt to a abs_exprt.
const irept & get_nil_irep()
const exprt & where() const
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
bitnot_exprt(const exprt &op)
The type of an expression.
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const typet &_type)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast a generic exprt to a isnormal_exprt.
unary_minus_exprt(const exprt &_op, const typet &_type)
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast a generic exprt to a function_application_exprt.
or_exprt(const exprt &op0, const exprt &op1)
const exprt & rhs() const
ieee_float_notequal_exprt()
binary_exprt(const irep_idt &_id)
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast a generic exprt to an extractbits_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast a generic exprt to an array_of_exprt.
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast a generic exprt to a bitor_exprt.
A generic base class for relations, i.e., binary predicates.
const exprt & value() const
if_exprt(const exprt &cond, const exprt &t, const exprt &f, const typet &type)
const exprt & lhs() const
shift_exprt(const irep_idt &_id, const typet &_type)
const member_designatort & to_member_designator(const exprt &expr)
Cast a generic exprt to an member_designatort.
application of (mathematical) function
binary_predicate_exprt(const irep_idt &_id)
index_exprt(const exprt &_array, const exprt &_index)
ieee_float_notequal_exprt(const exprt &_lhs, const exprt &_rhs)
const symbol_exprt & symbol() const
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast a generic exprt to a dynamic_object_exprt.
binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, const typet &_type)
complex_exprt(const complex_typet &_type)
Operator to update elements in structs and arrays.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast a generic exprt to a minus_exprt.
const exprt & pointer() const
Evaluates to true if the operand is infinite.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast a generic exprt to a multi_ary_exprt.
and_exprt(const exprt &op0, const exprt &op1, const exprt &op2)
unsigned int get_instance() const
member_exprt(const exprt &op)
const exprt & real() const
const exprt & array() const
unary_predicate_exprt(const irep_idt &_id)
void copy_to_operands(const exprt &expr)
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 member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
const irep_idt & get_value() const
const complex_exprt & to_complex_expr(const exprt &expr)
Cast a generic exprt to a complex_exprt.
The null pointer constant.
An expression denoting a type.
abs_exprt(const exprt &_op)
type_exprt(const typet &type)
plus_exprt(const exprt &_lhs, const exprt &_rhs, const typet &_type)
A transition system, consisting of state invariant, initial state predicate, and transition predicate...
bool is_thread_local() const
const exprt & root_object() const
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
The trinary if-then-else operator.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
std::size_t get_component_number() const
Evaluates to true if the operand is a normal number.
const exprt & where() const
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast a generic exprt to a isfinite_exprt.
A constant literal expression.
bool get_bool(const irep_namet &name) const
const exprt & index() const
symbol_exprt(const typet &type)
Constructor.
const exprt & where() const
irep_idt get_component_name() const
index_exprt(const typet &_type)
bool value_is_zero_string() const
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast a generic exprt to an extractbit_exprt.
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)
or_exprt(const exprt &op0, const exprt &op1, const exprt &op2, const exprt &op3)
const exprt & where() const
vector_exprt(const vector_typet &_type)
Extract member of struct or union.
const exprt & imag() const
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
const exprt & rounding_mode() const
void set_instance(unsigned int instance)
Concatenation of bit-vector operands.
update_exprt(const typet &_type)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
constant_exprt(const irep_idt &_value, const typet &_type)
void set_component_name(const irep_idt &component_name)
binary_predicate_exprt(const exprt &_op0, const irep_idt &_id, const exprt &_op1)
exprt conjunction(const exprt::operandst &)
const exprt & compound() const
replication_exprt(const typet &_type)
binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
decorated_symbol_exprt(const irep_idt &identifier)
Constructor.
if_exprt(const exprt &cond, const exprt &t, const exprt &f)
const irep_idt & id() const
unary_exprt(const irep_idt &_id)
dereference_exprt(const exprt &op, const typet &type)
const let_exprt & to_let_expr(const exprt &expr)
Cast a generic exprt to a let_exprt.
void set_value(const irep_idt &value)
const exprt & times() const
Evaluates to true if the operand is NaN.
An expression denoting infinity.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
shift_exprt(const exprt &_src, const irep_idt &_id, const exprt &_distance)
The boolean constant true.
member_exprt(const exprt &op, const irep_idt &component_name)
unary_exprt(const irep_idt &_id, const exprt &_op, const typet &_type)
const factorial_power_exprt & to_factorial_power_expr(const exprt &expr)
Cast a generic exprt to a factorial_power_exprt.
Expression to hold a symbol (variable)
division (integer and real)
binary_relation_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
A generic base class for binary expressions.
const exprt & invar() const
decorated_symbol_exprt(const irep_idt &identifier, const typet &type)
Constructor.
const exprt & distance() const
exprt::operandst argumentst
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
const and_exprt & to_and_expr(const exprt &expr)
Cast a generic exprt to a and_exprt.
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
unary_minus_exprt(const exprt &_op)
IEEE floating-point disequality.
member_exprt(const typet &_type)
Operator to dereference a pointer.
const update_exprt & to_update_expr(const exprt &expr)
Cast a generic exprt to an update_exprt.
A constant-size array type.
union constructor from single element
std::size_t get_component_number() const
factorial_power_exprt(const exprt &_base, const exprt &_exp)
const exprt & new_value() const
factorial_power_exprt & to_factorial_expr(exprt &expr)
Cast a generic exprt to a factorial_power_exprt.
not_exprt(const exprt &op)
const exprt & lhs() const
and_exprt(const exprt &op0, const exprt &op1)
binary_exprt(const irep_idt &_id, const typet &_type)
Generic base class for unary expressions.
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs)
infinity_exprt(const typet &_type)
const exprt & what() const
predicate_exprt(const irep_idt &_id, const exprt &_op)
unary_exprt(const irep_idt &_id, const exprt &_op)
#define PRECONDITION(CONDITION)
const exprt & false_case() const
typecast_exprt(const typet &_type)
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
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast a generic exprt to a isinf_exprt.
with_exprt(const exprt &_old, const exprt &_where, const exprt &_new_value)
symbol_exprt(const irep_idt &identifier, const typet &type)
Constructor.
const symbol_exprt & symbol() const
symbol_exprt(const irep_idt &identifier)
Constructor.
null_pointer_exprt(const pointer_typet &type)
ieee_float_equal_exprt(const exprt &_lhs, const exprt &_rhs)
const mod_exprt & to_mod_expr(const exprt &expr)
Cast a generic exprt to a mod_exprt.
predicate_exprt(const irep_idt &_id, const exprt &_op0, const exprt &_op1)
void set_static_lifetime()
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
array constructor from single element
multi_ary_exprt(const irep_idt &_id)
exprt disjunction(const exprt::operandst &)
power_exprt(const exprt &_base, const exprt &_exp)
isfinite_exprt(const exprt &op)
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast a generic exprt to an notequal_exprt.
vector constructor from list of elements
const exprt & old() const
const array_exprt & to_array_expr(const exprt &expr)
Cast a generic exprt to an array_exprt.
Operator to return the address of an object.
The unary minus expression.
concatenation_exprt(const exprt &_op0, const exprt &_op1, const typet &_type)
void set_component_number(std::size_t component_number)
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)
bool has_operands() const
const exprt & index() const
The boolean constant false.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast a generic exprt to a binary_exprt.
const exprt & init() const
const exprt & rhs() const
decorated_symbol_exprt(const typet &type)
Constructor.
equal_exprt(const exprt &_lhs, const exprt &_rhs)
const exprt & trans() const
std::vector< exprt > operandst
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast a generic exprt to an object_descriptor_exprt.
const exprt::operandst & designator() const
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
constant_exprt(const typet &type)
void clear_thread_local()
const ieee_float_equal_exprt & to_ieee_float_equal_expr(const exprt &expr)
Cast a generic exprt to an ieee_float_equal_exprt.
const index_designatort & to_index_designator(const exprt &expr)
Cast a generic exprt to an index_designatort.
const exprt & object() const
multi_ary_exprt(const irep_idt &_id, const typet &_type)
const symbol_exprt & symbol() const
minus_exprt(const exprt &_lhs, const exprt &_rhs)
index_designatort(const exprt &_index)
Complex numbers made of pair of given subtype.
dynamic_object_exprt(const typet &type)
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast a generic exprt to a concatenation_exprt.
typecast_exprt(const exprt &op, const typet &_type)
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast a generic exprt to a floatbv_typecast_exprt.
const exprt & old() const
const exprt & object() const
unary_exprt(const irep_idt &_id, const typet &_type)
plus_exprt(const exprt &_lhs, const exprt &_rhs)
update_exprt(const exprt &_old, const exprt &_designator, const exprt &_new_value)
const div_exprt & to_div_expr(const exprt &expr)
Cast a generic exprt to a div_exprt.
bitand_exprt(const exprt &_op0, const exprt &_op1)
const transt & to_trans_expr(const exprt &expr)
Cast a generic exprt to a transt.
shl_exprt(const exprt &_src, const exprt &_distance)
Evaluates to true if the operand is finite.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast a generic exprt to an ieee_float_op_exprt.
concatenation_exprt(const typet &_type)
ashr_exprt(const exprt &_src, const exprt &_distance)
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast a generic exprt to a isnan_exprt.
binary_relation_exprt(const irep_idt &id)
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.
floatbv_typecast_exprt(const exprt &op, const exprt &rounding, const typet &_type)
const exprt & struct_op() const
const exprt & rounding_mode() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
isnormal_exprt(const exprt &op)
const rem_exprt & to_rem_expr(const exprt &expr)
Cast a generic exprt to a rem_exprt.
const power_exprt & to_power_expr(const exprt &expr)
Cast a generic exprt to a power_exprt.
dereference_exprt(const exprt &op)
dereference_exprt(const typet &type)
Operator to update elements in structs and arrays.
const vector_exprt & to_vector_expr(const exprt &expr)
Cast a generic exprt to an vector_exprt.
sign_exprt(const exprt &_op)
lshr_exprt(const exprt &_src, const exprt &_distance)
unary_predicate_exprt(const irep_idt &_id, const exprt &_op)
irep_idt get_component_name() const
const exprt & offset() const
const plus_exprt & to_plus_expr(const exprt &expr)
Cast a generic exprt to a plus_exprt.
rem_exprt(const exprt &_lhs, const exprt &_rhs)
const mult_exprt & to_mult_expr(const exprt &expr)
Cast a generic exprt to a mult_exprt.
const exprt & valid() const
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast a generic exprt to a bitand_exprt.
const ieee_float_notequal_exprt & to_ieee_float_notequal_expr(const exprt &expr)
Cast a generic exprt to an ieee_float_notequal_exprt.
bitor_exprt(const exprt &_op0, const exprt &_op1)
const exprt & true_case() const
void set_identifier(const irep_idt &identifier)
array_exprt(const array_typet &_type)
irep_idt get_component_name() const
void set_component_name(const irep_idt &component_name)
and_exprt(const exprt &op0, const exprt &op1, const exprt &op2, const exprt &op3)
bool is_static_lifetime() const
isinf_exprt(const exprt &op)
isnan_exprt(const exprt &op)
Expression to hold a symbol (variable)
ashr_exprt(const exprt &_src, const std::size_t _distance)
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast a generic exprt to a bitxor_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast a generic exprt to a binary_relation_exprt.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast a generic exprt to a replication_exprt.
replication_exprt(const exprt &_times, const exprt &_src)
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
struct_exprt(const typet &_type)
void clear_static_lifetime()
#define DATA_INVARIANT(CONDITION, REASON)
A generic base class for multi-ary expressions.
mult_exprt(const exprt &_lhs, const exprt &_rhs)
mod_exprt(const exprt &_lhs, const exprt &_rhs)
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast a generic exprt to a bitnot_exprt.
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
std::size_t get_size_t(const irep_namet &name) const
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast a generic exprt to a unary_minus_exprt.
union_exprt(const typet &_type)
notequal_exprt(const exprt &_lhs, const exprt &_rhs)
complex_exprt(const exprt &_real, const exprt &_imag, const complex_typet &_type)
IEEE floating-point operations.
A base class for shift operators.
const argumentst & arguments() const
array constructor from list of elements
complex constructor from a pair of numbers
const implies_exprt & to_implies_expr(const exprt &expr)
Cast a generic exprt to a implies_exprt.
member_designatort(const irep_idt &_component_name)
array_of_exprt(const exprt &_what, const array_typet &_type)
const or_exprt & to_or_expr(const exprt &expr)
Cast a generic exprt to a or_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast a generic exprt to a unary_exprt.
A generic base class for expressions that are predicates, i.e., boolean-typed.
IEEE-floating-point equality.
address_of_exprt(const exprt &op, const pointer_typet &_type)
const exprt & new_value() const
function_application_exprt()