cprover
|
API to expression classes. More...
Go to the source code of this file.
Classes | |
class | transt |
A transition system, consisting of state invariant, initial state predicate, and transition predicate. More... | |
class | symbol_exprt |
Expression to hold a symbol (variable) More... | |
class | decorated_symbol_exprt |
Expression to hold a symbol (variable) More... | |
class | nondet_symbol_exprt |
Expression to hold a nondeterministic choice. More... | |
class | unary_exprt |
Generic base class for unary expressions. More... | |
class | abs_exprt |
absolute value More... | |
class | unary_minus_exprt |
The unary minus expression. More... | |
class | bswap_exprt |
The byte swap expression. More... | |
class | predicate_exprt |
A generic base class for expressions that are predicates, i.e., boolean-typed. More... | |
class | unary_predicate_exprt |
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly one argument. More... | |
class | sign_exprt |
sign of an expression More... | |
class | binary_exprt |
A generic base class for binary expressions. More... | |
class | binary_predicate_exprt |
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly two arguments. More... | |
class | binary_relation_exprt |
A generic base class for relations, i.e., binary predicates. More... | |
class | multi_ary_exprt |
A generic base class for multi-ary expressions. More... | |
class | plus_exprt |
The plus expression. More... | |
class | minus_exprt |
binary minus More... | |
class | mult_exprt |
binary multiplication More... | |
class | div_exprt |
division (integer and real) More... | |
class | mod_exprt |
binary modulo More... | |
class | rem_exprt |
remainder of division More... | |
class | power_exprt |
exponentiation More... | |
class | factorial_power_exprt |
falling factorial power More... | |
class | equal_exprt |
equality More... | |
class | notequal_exprt |
inequality More... | |
class | index_exprt |
array index operator More... | |
class | array_of_exprt |
array constructor from single element More... | |
class | array_exprt |
array constructor from list of elements More... | |
class | array_list_exprt |
Array constructor from a list of index-element pairs Operands are index/value pairs, alternating. More... | |
class | vector_exprt |
vector constructor from list of elements More... | |
class | union_exprt |
union constructor from single element More... | |
class | struct_exprt |
struct constructor from list of elements More... | |
class | complex_exprt |
complex constructor from a pair of numbers More... | |
class | object_descriptor_exprt |
split an expression into a base object and a (byte) offset More... | |
class | dynamic_object_exprt |
TO_BE_DOCUMENTED. More... | |
class | typecast_exprt |
semantic type conversion More... | |
class | floatbv_typecast_exprt |
semantic type conversion from/to floating-point formats More... | |
class | and_exprt |
boolean AND More... | |
class | implies_exprt |
boolean implication More... | |
class | or_exprt |
boolean OR More... | |
class | xor_exprt |
Boolean XOR. More... | |
class | bitnot_exprt |
Bit-wise negation of bit-vectors. More... | |
class | bitor_exprt |
Bit-wise OR. More... | |
class | bitxor_exprt |
Bit-wise XOR. More... | |
class | bitand_exprt |
Bit-wise AND. More... | |
class | shift_exprt |
A base class for shift operators. More... | |
class | shl_exprt |
Left shift. More... | |
class | ashr_exprt |
Arithmetic right shift. More... | |
class | lshr_exprt |
Logical right shift. More... | |
class | replication_exprt |
Bit-vector replication. More... | |
class | extractbit_exprt |
Extracts a single bit of a bit-vector operand. More... | |
class | extractbits_exprt |
Extracts a sub-range of a bit-vector operand. More... | |
class | address_of_exprt |
Operator to return the address of an object. More... | |
class | not_exprt |
Boolean negation. More... | |
class | dereference_exprt |
Operator to dereference a pointer. More... | |
class | if_exprt |
The trinary if-then-else operator. More... | |
class | with_exprt |
Operator to update elements in structs and arrays. More... | |
class | index_designatort |
class | member_designatort |
class | update_exprt |
Operator to update elements in structs and arrays. More... | |
class | member_exprt |
Extract member of struct or union. More... | |
class | isnan_exprt |
Evaluates to true if the operand is NaN. More... | |
class | isinf_exprt |
Evaluates to true if the operand is infinite. More... | |
class | isfinite_exprt |
Evaluates to true if the operand is finite. More... | |
class | isnormal_exprt |
Evaluates to true if the operand is a normal number. More... | |
class | ieee_float_equal_exprt |
IEEE-floating-point equality. More... | |
class | ieee_float_notequal_exprt |
IEEE floating-point disequality. More... | |
class | ieee_float_op_exprt |
IEEE floating-point operations. More... | |
class | type_exprt |
An expression denoting a type. More... | |
class | constant_exprt |
A constant literal expression. More... | |
class | true_exprt |
The boolean constant true. More... | |
class | false_exprt |
The boolean constant false. More... | |
class | nil_exprt |
The NIL expression. More... | |
class | null_pointer_exprt |
The null pointer constant. More... | |
class | function_application_exprt |
application of (mathematical) function More... | |
class | concatenation_exprt |
Concatenation of bit-vector operands. More... | |
class | infinity_exprt |
An expression denoting infinity. More... | |
class | let_exprt |
A let expression. More... | |
class | quantifier_exprt |
A base class for quantifier expressions. More... | |
class | forall_exprt |
A forall expression. More... | |
class | exists_exprt |
An exists expression. More... | |
class | popcount_exprt |
The popcount (counting the number of bits set to 1) expression. More... | |
|
inline |
Definition at line 432 of file std_expr.h.
|
inline |
Definition at line 3218 of file std_expr.h.
|
inline |
Definition at line 2327 of file std_expr.h.
|
inline |
Definition at line 1655 of file std_expr.h.
|
inline |
Definition at line 1672 of file std_expr.h.
|
inline |
Definition at line 1605 of file std_expr.h.
|
inline |
Definition at line 721 of file std_expr.h.
Referenced by can_cast_expr< binary_relation_exprt >().
|
inline |
Definition at line 822 of file std_expr.h.
References can_cast_expr< binary_exprt >().
|
inline |
Definition at line 2749 of file std_expr.h.
|
inline |
Definition at line 2571 of file std_expr.h.
|
inline |
Definition at line 2628 of file std_expr.h.
|
inline |
Definition at line 2688 of file std_expr.h.
|
inline |
Definition at line 564 of file std_expr.h.
|
inline |
Definition at line 1931 of file std_expr.h.
|
inline |
Definition at line 4676 of file std_expr.h.
|
inline |
Definition at line 4480 of file std_expr.h.
|
inline |
Definition at line 3349 of file std_expr.h.
|
inline |
Definition at line 1121 of file std_expr.h.
|
inline |
Definition at line 2098 of file std_expr.h.
|
inline |
Definition at line 1394 of file std_expr.h.
|
inline |
Definition at line 3060 of file std_expr.h.
|
inline |
Definition at line 3158 of file std_expr.h.
|
inline |
Definition at line 1341 of file std_expr.h.
|
inline |
Definition at line 2243 of file std_expr.h.
|
inline |
Definition at line 4608 of file std_expr.h.
Referenced by string_refinementt::dec_solve().
|
inline |
Definition at line 4245 of file std_expr.h.
|
inline |
Definition at line 4304 of file std_expr.h.
|
inline |
Definition at line 3447 of file std_expr.h.
|
inline |
Definition at line 2379 of file std_expr.h.
|
inline |
Definition at line 3604 of file std_expr.h.
|
inline |
Definition at line 1538 of file std_expr.h.
|
inline |
Definition at line 4136 of file std_expr.h.
|
inline |
Definition at line 4084 of file std_expr.h.
|
inline |
Definition at line 4028 of file std_expr.h.
|
inline |
Definition at line 4188 of file std_expr.h.
|
inline |
Definition at line 4772 of file std_expr.h.
|
inline |
Definition at line 3660 of file std_expr.h.
|
inline |
Definition at line 3976 of file std_expr.h.
|
inline |
Definition at line 1005 of file std_expr.h.
|
inline |
Definition at line 1175 of file std_expr.h.
|
inline |
Definition at line 1063 of file std_expr.h.
|
inline |
Definition at line 291 of file std_expr.h.
|
inline |
Definition at line 3271 of file std_expr.h.
|
inline |
Definition at line 1450 of file std_expr.h.
|
inline |
Definition at line 2023 of file std_expr.h.
|
inline |
Definition at line 2463 of file std_expr.h.
|
inline |
Definition at line 947 of file std_expr.h.
|
inline |
Definition at line 4936 of file std_expr.h.
|
inline |
Definition at line 1283 of file std_expr.h.
|
inline |
Definition at line 4847 of file std_expr.h.
|
inline |
Definition at line 1229 of file std_expr.h.
|
inline |
Definition at line 2979 of file std_expr.h.
|
inline |
Definition at line 1853 of file std_expr.h.
|
inline |
Definition at line 227 of file std_expr.h.
Referenced by references_class_model().
|
inline |
Definition at line 78 of file std_expr.h.
|
inline |
Definition at line 2164 of file std_expr.h.
|
inline |
Definition at line 380 of file std_expr.h.
|
inline |
Definition at line 495 of file std_expr.h.
|
inline |
Definition at line 1803 of file std_expr.h.
|
inline |
Definition at line 3762 of file std_expr.h.
|
inline |
Definition at line 1722 of file std_expr.h.
|
inline |
Definition at line 3540 of file std_expr.h.
Referenced by sparse_arrayt::sparse_arrayt().
|
inline |
Definition at line 2513 of file std_expr.h.
exprt conjunction | ( | const exprt::operandst & | ) |
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) returns true otherwise
Definition at line 48 of file std_expr.cpp.
References exprt::operands().
Referenced by string_constraint_generatort::add_axioms_for_characters_in_integer_string(), string_constraint_generatort::add_axioms_for_fractional_part(), bmc_all_propertiest::goalt::as_expr(), partial_order_concurrencyt::before(), collect_mcdc_controlling_rec(), acceleration_utilst::do_arrays(), instantiate(), instantiate_quantifier(), instrument_intervals(), interval_domaint::make_expression(), negation_of_not_contains_constraint(), operator-=(), operator|=(), and replacement_conjunction().
exprt disjunction | ( | const exprt::operandst & | ) |
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) returns false otherwise
Definition at line 24 of file std_expr.cpp.
References exprt::operands().
Referenced by string_constraint_generatort::add_axioms_for_intern(), string_constraint_generatort::add_axioms_for_to_lower_case(), bmc_covert::goalt::as_expr(), cover_goalst::constraint(), symex_target_equationt::convert_assertions(), character_refine_preprocesst::expr_of_is_defined(), character_refine_preprocesst::expr_of_is_title_case(), character_refine_preprocesst::expr_of_is_unicode_identifier_part(), character_refine_preprocesst::expr_of_is_whitespace(), character_refine_preprocesst::in_list_expr(), instantiate_quantifier(), remove_instanceoft::lower_instanceof(), float_bvt::mul(), and goto_checkt::pointer_validity_check().
Cast a generic exprt to a abs_exprt.
This is an unchecked conversion. expr must be known to be abs_exprt.
expr | Source expression |
Definition at line 411 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by float_bvt::convert(), and boolbvt::convert_bitvector().
Cast a generic exprt to a abs_exprt.
This is an unchecked conversion. expr must be known to be abs_exprt.
expr | Source expression |
Definition at line 423 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an address_of_exprt.
This is an unchecked conversion. expr must be known to be address_of_exprt.
expr | Source expression |
Definition at line 3201 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by goto_symext::address_arithmetic(), string_abstractiont::build_pointer(), goto_symex_statet::constant_propagation(), goto_program2codet::convert_assign_varargs(), dereferencet::dereference_rec(), goto_symext::dereference_rec(), dirtyt::find_dirty(), custom_bitvector_analysist::get_bit_nr(), escape_domaint::get_function(), rw_range_sett::get_objects_rec(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), global_may_alias_domaint::get_rhs_aliases(), escape_domaint::get_rhs_aliases(), get_symbol(), constant_propagator_domaint::valuest::is_constant(), array_poolt::make_char_array_for_char_pointer(), custom_bitvector_domaint::object2id(), goto_symext::process_array_expr(), replace_symbolt::replace(), require_goto_statements::require_entry_point_argument_assignment(), require_goto_statements::require_struct_component_assignment(), rewrite_union(), simplify_exprt::simplify_dereference(), simplify_exprt::simplify_typecast(), remove_const_function_pointerst::try_resolve_dereference(), and remove_const_function_pointerst::try_resolve_function_call().
|
inline |
Cast a generic exprt to an address_of_exprt.
This is an unchecked conversion. expr must be known to be address_of_exprt.
expr | Source expression |
Definition at line 3211 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Cast a generic exprt to a and_exprt.
This is an unchecked conversion. expr must be known to be and_exprt.
expr | Source expression |
Definition at line 2306 of file std_expr.h.
References irept::id(), and PRECONDITION.
Cast a generic exprt to a and_exprt.
This is an unchecked conversion. expr must be known to be and_exprt.
expr | Source expression |
Definition at line 2318 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to an array_exprt.
This is an unchecked conversion. expr must be known to be array_exprt.
expr | Source expression |
Definition at line 1640 of file std_expr.h.
References irept::id(), and PRECONDITION.
Referenced by string_constraint_generatort::add_axioms_for_format(), string_abstractiont::build(), and rw_range_sett::get_objects_rec().
|
inline |
Cast a generic exprt to an array_exprt.
This is an unchecked conversion. expr must be known to be array_exprt.
expr | Source expression |
Definition at line 1649 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to an array_of_exprt.
This is an unchecked conversion. expr must be known to be array_of_exprt.
expr | Source expression |
Definition at line 1584 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by arrayst::add_array_constraints(), and boolbvt::convert_bitvector().
|
inline |
Cast a generic exprt to an array_of_exprt.
This is an unchecked conversion. expr must be known to be array_of_exprt.
expr | Source expression |
Definition at line 1596 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a binary_exprt.
This is an unchecked conversion. expr must be known to be binary_exprt.
expr | Source expression |
Definition at line 702 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
Referenced by boolbvt::convert_bitvector(), and format_rec().
|
inline |
Cast a generic exprt to a binary_exprt.
This is an unchecked conversion. expr must be known to be binary_exprt.
expr | Source expression |
Definition at line 713 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
|
inline |
Cast a generic exprt to a binary_relation_exprt.
This is an unchecked conversion. expr must be known to be binary_relation_exprt.
expr | Source expression |
Definition at line 803 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
Referenced by boolbvt::convert_rest(), and c_typecheck_baset::typecheck_expr_main().
|
inline |
Cast a generic exprt to a binary_relation_exprt.
This is an unchecked conversion. expr must be known to be binary_relation_exprt.
expr | Source expression |
Definition at line 814 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
|
inline |
Cast a generic exprt to a bitand_exprt.
This is an unchecked conversion. expr must be known to be bitand_exprt.
expr | Source expression |
Definition at line 2728 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a bitand_exprt.
This is an unchecked conversion. expr must be known to be bitand_exprt.
expr | Source expression |
Definition at line 2740 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a bitnot_exprt.
This is an unchecked conversion. expr must be known to be bitnot_exprt.
expr | Source expression |
Definition at line 2552 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a bitnot_exprt.
This is an unchecked conversion. expr must be known to be bitnot_exprt.
expr | Source expression |
Definition at line 2563 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a bitor_exprt.
This is an unchecked conversion. expr must be known to be bitor_exprt.
expr | Source expression |
Definition at line 2607 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a bitor_exprt.
This is an unchecked conversion. expr must be known to be bitor_exprt.
expr | Source expression |
Definition at line 2619 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a bitxor_exprt.
This is an unchecked conversion. expr must be known to be bitxor_exprt.
expr | Source expression |
Definition at line 2667 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a bitxor_exprt.
This is an unchecked conversion. expr must be known to be bitxor_exprt.
expr | Source expression |
Definition at line 2679 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a bswap_exprt.
This is an unchecked conversion. expr must be known to be bswap_exprt.
expr | Source expression |
Definition at line 542 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::op0(), exprt::operands(), PRECONDITION, and exprt::type().
Referenced by boolbvt::convert_bitvector(), and simplify_exprt::simplify_node().
|
inline |
Cast a generic exprt to a bswap_exprt.
This is an unchecked conversion. expr must be known to be bswap_exprt.
expr | Source expression |
Definition at line 554 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::op0(), exprt::operands(), PRECONDITION, and exprt::type().
|
inline |
Cast a generic exprt to a complex_exprt.
This is an unchecked conversion. expr must be known to be complex_exprt.
expr | Source expression |
Definition at line 1910 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a complex_exprt.
This is an unchecked conversion. expr must be known to be complex_exprt.
expr | Source expression |
Definition at line 1922 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a concatenation_exprt.
This is an unchecked conversion. expr must be known to be concatenation_exprt.
expr | Source expression |
Definition at line 4655 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a concatenation_exprt.
This is an unchecked conversion. expr must be known to be concatenation_exprt.
expr | Source expression |
Definition at line 4667 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a constant_exprt.
This is an unchecked conversion. expr must be known to be constant_exprt.
expr | Source expression |
Definition at line 4465 of file std_expr.h.
References irept::id(), and PRECONDITION.
Referenced by string_constraint_generatort::add_axioms_for_constrain_characters(), string_constraint_generatort::add_axioms_for_format(), interval_domaint::assume_rec(), build_ssa_identifier_rec(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), goto_program2codet::convert_assign_varargs(), boolbvt::convert_bitvector(), java_bytecode_convert_methodt::convert_const(), expr2javat::convert_constant(), expr2ct::convert_constant(), smt2_convt::convert_expr(), java_bytecode_convert_methodt::convert_instructions(), bv_pointerst::convert_pointer_type(), smt2_convt::convert_rounding_mode_FPA(), java_bytecode_convert_methodt::convert_switch(), expr2javat::convert_with_precedence(), expr2cppt::convert_with_precedence(), expr2ct::convert_with_precedence(), dereferencet::dereference_rec(), simplify_exprt::eliminate_common_addends(), custom_bitvector_domaint::eval(), interpretert::evaluate(), simplify_exprt::expr2bits(), acceleration_utilst::extract_polynomial(), polynomial_acceleratort::fit_const(), format_rec(), polynomialt::from_expr(), dynamic_object_exprt::get_instance(), goto_convertt::get_string_constant(), is_dereference_integer_object(), exprt::is_one(), is_store_to_slot(), exprt::is_zero(), json(), mul_expr(), format_constantt::operator()(), numeric_castt< mp_integer >::operator()(), smt2_convt::parse_struct(), require_expr::require_index(), simplify_exprt::simplify_abs(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_div(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_ieee_float_relation(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_isinf(), simplify_exprt::simplify_isnan(), simplify_exprt::simplify_isnormal(), simplify_json_expr(), simplify_exprt::simplify_mult(), simplify_exprt::simplify_plus(), simplify_exprt::simplify_pointer_offset(), simplify_exprt::simplify_sign(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_unary_minus(), sum_expr(), sum_over_map(), to_integer(), custom_bitvector_domaint::transform(), remove_const_function_pointerst::try_resolve_index_value(), c_typecheck_baset::typecheck_expr_trinary(), unsigned_from_ns(), utf16_constant_array_to_java(), java_bytecode_convert_methodt::variable(), and xml().
|
inline |
Cast a generic exprt to a constant_exprt.
This is an unchecked conversion. expr must be known to be constant_exprt.
expr | Source expression |
Definition at line 4474 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a dereference_exprt.
This is an unchecked conversion. expr must be known to be dereference_exprt.
expr | Source expression |
Definition at line 3328 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by string_abstractiont::abstract_char_assign(), goto_symext::address_arithmetic(), ai_domain_baset::ai_simplify_lhs(), custom_bitvector_analysist::aliases(), goto_checkt::bounds_check(), string_abstractiont::build(), goto_checkt::check_rec(), collect_deref_expr(), goto_program2codet::convert_assign_varargs(), dirtyt::find_dirty_address_of(), function_modifiest::get_modifies_lhs(), get_modifies_lhs(), get_objects_rec(), rw_range_sett::get_objects_rec(), java_bytecode_instrumentt::instrument_expr(), constant_propagator_domaint::valuest::is_constant_address_of(), mm_io(), nondet_volatile_lhs(), custom_bitvector_domaint::object2id(), rewrite_union_address_of(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_dereference(), remove_const_function_pointerst::try_resolve_expression(), and remove_const_function_pointerst::try_resolve_function_call().
|
inline |
Cast a generic exprt to a dereference_exprt.
This is an unchecked conversion. expr must be known to be dereference_exprt.
expr | Source expression |
Definition at line 3340 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Cast a generic exprt to a div_exprt.
This is an unchecked conversion. expr must be known to be div_exprt.
expr | Source expression |
Definition at line 1100 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by goto_checkt::check_rec(), boolbvt::convert_bitvector(), and smt2_convt::convert_expr().
Cast a generic exprt to a div_exprt.
This is an unchecked conversion. expr must be known to be div_exprt.
expr | Source expression |
Definition at line 1112 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a dynamic_object_exprt.
This is an unchecked conversion. expr must be known to be dynamic_object_exprt.
expr | Source expression |
Definition at line 2076 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by value_set_fit::assign_rec(), value_set_fivrnst::assign_rec(), value_set_fivrt::assign_rec(), value_sett::assign_rec(), value_set_fit::do_free(), value_set_fivrnst::do_free(), value_set_fivrt::do_free(), value_sett::do_free(), value_set_fit::get_value_set_rec(), value_set_fivrnst::get_value_set_rec(), value_set_fivrt::get_value_set_rec(), and value_sett::get_value_set_rec().
|
inline |
Cast a generic exprt to a dynamic_object_exprt.
This is an unchecked conversion. expr must be known to be dynamic_object_exprt.
expr | Source expression |
Definition at line 2089 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an equal_exprt.
This is an unchecked conversion. expr must be known to be equal_exprt.
expr | Source expression |
Definition at line 1377 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by boolbvt::convert_equality(), goto_program2codet::convert_goto_switch(), boolbvt::convert_rest(), bdd_exprt::from_expr_rec(), goto_program2codet::get_cases(), string_refinementt::set_to(), prop_conv_solvert::set_to(), and smt2_convt::set_to().
|
inline |
Cast a generic exprt to an equal_exprt.
This is an unchecked conversion. expr must be known to be equal_exprt.
expr | Source expression |
Definition at line 1387 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an extractbit_exprt.
This is an unchecked conversion. expr must be known to be extractbit_exprt.
expr | Source expression |
Definition at line 3039 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by boolbvt::convert_rest(), qbf_bdd_certificatet::f_get(), and qbf_squolem_coret::f_get().
|
inline |
Cast a generic exprt to an extractbit_exprt.
This is an unchecked conversion. expr must be known to be extractbit_exprt.
expr | Source expression |
Definition at line 3051 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an extractbits_exprt.
This is an unchecked conversion. expr must be known to be extractbits_exprt.
expr | Source expression |
Definition at line 3137 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by boolbvt::convert_bitvector(), and simplify_exprt::simplify_node().
|
inline |
Cast a generic exprt to an extractbits_exprt.
This is an unchecked conversion. expr must be known to be extractbits_exprt.
expr | Source expression |
Definition at line 3149 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a factorial_power_exprt.
This is an unchecked conversion. expr must be known to be factorial_power_exprt.
expr | Source expression |
Definition at line 1332 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a factorial_power_exprt.
This is an unchecked conversion. expr must be known to be factorial_power_exprt.
expr | Source expression |
Definition at line 1320 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a floatbv_typecast_exprt.
This is an unchecked conversion. expr must be known to be floatbv_typecast_exprt.
expr | Source expression |
Definition at line 2221 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by boolbvt::convert_bitvector(), and smt2_convt::convert_expr().
|
inline |
Cast a generic exprt to a floatbv_typecast_exprt.
This is an unchecked conversion. expr must be known to be floatbv_typecast_exprt.
expr | Source expression |
Definition at line 2233 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a function_application_exprt.
This is an unchecked conversion. expr must be known to be function_application_exprt.
expr | Source expression |
Definition at line 4585 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by boolbvt::convert_bitvector(), expr2ct::convert_with_precedence(), and smt2_solvert::expand_function_applications().
|
inline |
Cast a generic exprt to a function_application_exprt.
This is an unchecked conversion. expr must be known to be function_application_exprt.
expr | Source expression |
Definition at line 4598 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an ieee_float_equal_exprt.
This is an unchecked conversion. expr must be known to be ieee_float_equal_exprt.
expr | Source expression |
Definition at line 4223 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an ieee_float_equal_exprt.
This is an unchecked conversion. expr must be known to be ieee_float_equal_exprt.
expr | Source expression |
Definition at line 4235 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an ieee_float_notequal_exprt.
This is an unchecked conversion. expr must be known to be ieee_float_notequal_exprt.
expr | Source expression |
Definition at line 4281 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an ieee_float_notequal_exprt.
This is an unchecked conversion. expr must be known to be ieee_float_notequal_exprt.
expr | Source expression |
Definition at line 4294 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an ieee_float_op_exprt.
This is an unchecked conversion. expr must be known to be ieee_float_op_exprt.
expr | Source expression |
Definition at line 4375 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
Referenced by smt2_convt::convert_expr().
|
inline |
Cast a generic exprt to an ieee_float_op_exprt.
This is an unchecked conversion. expr must be known to be ieee_float_op_exprt.
expr | Source expression |
Definition at line 4386 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
Cast a generic exprt to an if_exprt.
This is an unchecked conversion. expr must be known to be if_exprt.
expr | Source expression |
Definition at line 3426 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by arrayst::add_array_constraints(), goto_symext::address_arithmetic(), local_may_aliast::assign_lhs(), local_bitvector_analysist::assign_lhs(), string_abstractiont::build(), build_full_lhs_rec(), goto_convertt::clean_expr(), arrayst::collect_arrays(), rw_set_functiont::compute_rec(), bv_pointerst::convert_address_of_rec(), boolbvt::convert_bitvector(), goto_convertt::convert_expression(), bv_pointerst::convert_pointer_type(), value_set_dereferencet::dereference(), dereferencet::dereference_rec(), goto_symext::dereference_rec_address_of(), goto_convertt::do_function_call(), eval_string(), dirtyt::find_dirty_address_of(), for_each_atomic_string(), format_rec(), bdd_exprt::from_expr_rec(), function_modifiest::get_modifies_function(), function_modifiest::get_modifies_lhs(), get_modifies_lhs(), rw_range_sett::get_objects_address_of(), get_objects_rec(), rw_range_sett::get_objects_rec(), local_may_aliast::get_rec(), custom_bitvector_domaint::get_rhs(), global_may_alias_domaint::get_rhs_aliases(), escape_domaint::get_rhs_aliases(), global_may_alias_domaint::get_rhs_aliases_address_of(), escape_domaint::get_rhs_aliases_address_of(), escape_domaint::get_rhs_cleanup(), get_sub_arrays(), interval_domaint::havoc_rec(), goto_symext::havoc_rec(), goto_symext::is_index_member_symbol_if(), lift_if(), array_poolt::make_char_array_for_char_pointer(), nondet_volatile_lhs(), goto_symext::process_array_expr(), goto_symex_statet::rename(), goto_symex_statet::rename_address(), simplify_exprt::simplify_dereference(), simplify_exprt::simplify_if(), simplify_exprt::simplify_index(), simplify_exprt::simplify_member(), simplify_exprt::simplify_node(), simplify_exprt::simplify_node_preorder(), simplify_exprt::simplify_pointer_object(), simplify_exprt::simplify_typecast(), goto_symext::symex_assign_rec(), c_typecheck_baset::typecheck_expr_main(), and string_abstractiont::value_assignments().
Cast a generic exprt to an if_exprt.
This is an unchecked conversion. expr must be known to be if_exprt.
expr | Source expression |
Definition at line 3438 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a implies_exprt.
This is an unchecked conversion. expr must be known to be implies_exprt.
expr | Source expression |
Definition at line 2362 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by bv_refinementt::arrays_overapproximated(), and bdd_exprt::from_expr_rec().
|
inline |
Cast a generic exprt to a implies_exprt.
This is an unchecked conversion. expr must be known to be implies_exprt.
expr | Source expression |
Definition at line 2372 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an index_designatort.
This is an unchecked conversion. expr must be known to be index_designatort.
expr | Source expression |
Definition at line 3583 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by make_with_expr().
|
inline |
Cast a generic exprt to an index_designatort.
This is an unchecked conversion. expr must be known to be index_designatort.
expr | Source expression |
Definition at line 3595 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an index_exprt.
This is an unchecked conversion. expr must be known to be index_exprt.
expr | Source expression |
Definition at line 1517 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by string_abstractiont::abstract_char_assign(), ai_domain_baset::ai_simplify_lhs(), acceleration_utilst::array_assignments2polys(), uninitialized_domaint::assign(), local_may_aliast::assign_lhs(), local_bitvector_analysist::assign_lhs(), string_constraint_generatort::associate_array_to_pointer(), string_abstractiont::build(), build_full_lhs_rec(), build_object_descriptor_rec(), string_abstractiont::build_pointer(), build_ssa_identifier_rec(), goto_checkt::check_rec(), arrayst::collect_indices(), compute_pointer_offset(), goto_symex_statet::constant_propagation_reference(), bv_pointerst::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), boolbvt::convert_bitvector(), smt2_convt::convert_expr(), bv_pointerst::convert_pointer_type(), boolbvt::convert_rest(), expr2ct::convert_with_precedence(), goto_symext::dereference_rec(), goto_symext::dereference_rec_address_of(), dirtyt::find_dirty_address_of(), find_indexes(), format_rec(), acceleration_utilst::gather_array_assignments(), custom_bitvector_analysist::get_bit_nr(), rw_range_sett::get_objects_address_of(), get_objects_rec(), rw_range_sett::get_objects_rec(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), value_sett::get_reference_set_rec(), goto_symext::havoc_rec(), initial_index_set(), goto_checkt::invalidate(), constant_propagator_domaint::valuest::is_constant_address_of(), goto_symext::is_index_member_symbol_if(), is_lvalue(), boolbvt::literal(), array_poolt::make_char_array_for_char_pointer(), goto_convertt::needs_cleaning(), nondet_volatile_lhs(), goto_symext::process_array_expr(), pointer_arithmetict::read(), dereferencet::read_object(), goto_symex_statet::rename_address(), replace_symbolt::replace(), require_expr::require_index(), require_expr::require_top_index(), rewrite_assignment(), rewrite_union_address_of(), simplify_exprt::simplify_address_of(), simplify_exprt::simplify_dereference(), simplify_exprt::simplify_index(), simplify_exprt::simplify_inequality_address_of(), simplify_json_expr(), goto_symext::symex_assign_rec(), remove_const_function_pointerst::try_resolve_expression(), and remove_const_function_pointerst::try_resolve_function_call().
|
inline |
Cast a generic exprt to an index_exprt.
This is an unchecked conversion. expr must be known to be index_exprt.
expr | Source expression |
Definition at line 1529 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a isfinite_exprt.
This is an unchecked conversion. expr must be known to be isfinite_exprt.
expr | Source expression |
Definition at line 4119 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a isfinite_exprt.
This is an unchecked conversion. expr must be known to be isfinite_exprt.
expr | Source expression |
Definition at line 4129 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a isinf_exprt.
This is an unchecked conversion. expr must be known to be isinf_exprt.
expr | Source expression |
Definition at line 4063 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a isinf_exprt.
This is an unchecked conversion. expr must be known to be isinf_exprt.
expr | Source expression |
Definition at line 4075 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a isnan_exprt.
This is an unchecked conversion. expr must be known to be isnan_exprt.
expr | Source expression |
Definition at line 4011 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a isnan_exprt.
This is an unchecked conversion. expr must be known to be isnan_exprt.
expr | Source expression |
Definition at line 4021 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a isnormal_exprt.
This is an unchecked conversion. expr must be known to be isnormal_exprt.
expr | Source expression |
Definition at line 4171 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a isnormal_exprt.
This is an unchecked conversion. expr must be known to be isnormal_exprt.
expr | Source expression |
Definition at line 4181 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Cast a generic exprt to a let_exprt.
This is an unchecked conversion. expr must be known to be let_exprt.
expr | Source expression |
Definition at line 4755 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by boolbvt::convert_bitvector(), prop_conv_solvert::convert_bool(), smt2_convt::convert_expr(), boolbvt::convert_rest(), expr2ct::convert_with_precedence(), and format_rec().
Cast a generic exprt to a let_exprt.
This is an unchecked conversion. expr must be known to be let_exprt.
expr | Source expression |
Definition at line 4765 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an member_designatort.
This is an unchecked conversion. expr must be known to be member_designatort.
expr | Source expression |
Definition at line 3639 of file std_expr.h.
References DATA_INVARIANT, exprt::has_operands(), irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to an member_designatort.
This is an unchecked conversion. expr must be known to be member_designatort.
expr | Source expression |
Definition at line 3651 of file std_expr.h.
References DATA_INVARIANT, exprt::has_operands(), irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a member_exprt.
This is an unchecked conversion. expr must be known to be member_exprt.
expr | Source expression |
Definition at line 3955 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by arrayst::add_array_constraints(), ai_domain_baset::ai_simplify_lhs(), uninitialized_domaint::assign(), local_may_aliast::assign_lhs(), local_bitvector_analysist::assign_lhs(), string_abstractiont::build(), build_full_lhs_rec(), build_object_descriptor_rec(), build_ssa_identifier_rec(), goto_checkt::check_rec(), arrayst::collect_arrays(), compute_pointer_offset(), bv_pointerst::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), graphml_witnesst::convert_assign_rec(), boolbvt::convert_bitvector(), smt2_convt::convert_expr(), smt2_convt::convert_member(), bv_pointerst::convert_pointer_type(), boolbvt::convert_rest(), expr2ct::convert_with_precedence(), goto_symext::dereference_rec_address_of(), interpretert::evaluate_address(), dirtyt::find_dirty_address_of(), require_goto_statements::find_struct_component_assignments(), require_goto_statements::find_this_component_assignment(), format_rec(), smt2_convt::get(), rw_range_sett::get_objects_address_of(), get_objects_rec(), rw_range_sett::get_objects_rec(), have_to_rewrite_union(), goto_symext::havoc_rec(), java_bytecode_instrumentt::instrument_expr(), goto_checkt::invalidate(), constant_propagator_domaint::valuest::is_constant_address_of(), goto_symext::is_index_member_symbol_if(), is_lvalue(), boolbvt::literal(), nondet_volatile_lhs(), custom_bitvector_domaint::object2id(), dereferencet::read_object(), goto_symex_statet::rename_address(), replace_symbolt::replace(), require_expr::require_member(), rewrite_assignment(), rewrite_union(), rewrite_union_address_of(), java_bytecode_convert_methodt::save_stack_entries(), simplify_exprt::simplify_address_of_arg(), simplify_json_expr(), simplify_exprt::simplify_member(), goto_symext::symex_assign_rec(), remove_const_function_pointerst::try_resolve_expression(), remove_const_function_pointerst::try_resolve_function_call(), and java_bytecode_typecheckt::typecheck_expr().
|
inline |
Cast a generic exprt to a member_exprt.
This is an unchecked conversion. expr must be known to be member_exprt.
expr | Source expression |
Definition at line 3967 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a minus_exprt.
This is an unchecked conversion. expr must be known to be minus_exprt.
expr | Source expression |
Definition at line 984 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by smt2_convt::convert_expr().
|
inline |
Cast a generic exprt to a minus_exprt.
This is an unchecked conversion. expr must be known to be minus_exprt.
expr | Source expression |
Definition at line 996 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Cast a generic exprt to a mod_exprt.
This is an unchecked conversion. expr must be known to be mod_exprt.
expr | Source expression |
Definition at line 1158 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by goto_checkt::check_rec(), boolbvt::convert_bitvector(), and smt2_convt::convert_expr().
Cast a generic exprt to a mod_exprt.
This is an unchecked conversion. expr must be known to be mod_exprt.
expr | Source expression |
Definition at line 1168 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a mult_exprt.
This is an unchecked conversion. expr must be known to be mult_exprt.
expr | Source expression |
Definition at line 1042 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by smt2_convt::convert_expr().
|
inline |
Cast a generic exprt to a mult_exprt.
This is an unchecked conversion. expr must be known to be mult_exprt.
expr | Source expression |
Definition at line 1054 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a multi_ary_exprt.
This is an unchecked conversion. expr must be known to be multi_ary_exprt.
expr | Source expression |
Definition at line 877 of file std_expr.h.
Referenced by format_rec().
|
inline |
Cast a generic exprt to a multi_ary_exprt.
This is an unchecked conversion. expr must be known to be multi_ary_exprt.
expr | Source expression |
Definition at line 885 of file std_expr.h.
|
inline |
Cast a generic exprt to a nondet_symbol_exprt.
This is an unchecked conversion. expr must be known to be nondet_symbol_exprt.
expr | Source expression |
Definition at line 274 of file std_expr.h.
References DATA_INVARIANT, exprt::has_operands(), irept::id(), and PRECONDITION.
Referenced by smt2_convt::convert_expr(), expr2ct::convert_with_precedence(), smt2_convt::find_symbols(), and smt2_convt::get().
|
inline |
Cast a generic exprt to a nondet_symbol_exprt.
This is an unchecked conversion. expr must be known to be nondet_symbol_exprt.
expr | Source expression |
Definition at line 284 of file std_expr.h.
References DATA_INVARIANT, exprt::has_operands(), irept::id(), and PRECONDITION.
Cast a generic exprt to an not_exprt.
This is an unchecked conversion. expr must be known to be not_exprt.
expr | Source expression |
Definition at line 3254 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by interval_domaint::assume_rec(), collect_mcdc_controlling_rec(), boolbvt::convert_bitvector(), and bdd_exprt::from_expr_rec().
Cast a generic exprt to an not_exprt.
This is an unchecked conversion. expr must be known to be not_exprt.
expr | Source expression |
Definition at line 3264 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an notequal_exprt.
This is an unchecked conversion. expr must be known to be notequal_exprt.
expr | Source expression |
Definition at line 1429 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an notequal_exprt.
This is an unchecked conversion. expr must be known to be notequal_exprt.
expr | Source expression |
Definition at line 1441 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an object_descriptor_exprt.
This is an unchecked conversion. expr must be known to be object_descriptor_exprt.
expr | Source expression |
Definition at line 2000 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by value_set_dereferencet::build_reference_to(), flow_insensitive_analysis_baset::do_function_call_rec(), and static_analysis_baset::do_function_call_rec().
|
inline |
Cast a generic exprt to an object_descriptor_exprt.
This is an unchecked conversion. expr must be known to be object_descriptor_exprt.
expr | Source expression |
Definition at line 2013 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Cast a generic exprt to a or_exprt.
This is an unchecked conversion. expr must be known to be or_exprt.
expr | Source expression |
Definition at line 2442 of file std_expr.h.
References irept::id(), and PRECONDITION.
Referenced by bv_refinementt::arrays_overapproximated().
Cast a generic exprt to a or_exprt.
This is an unchecked conversion. expr must be known to be or_exprt.
expr | Source expression |
Definition at line 2454 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a plus_exprt.
This is an unchecked conversion. expr must be known to be plus_exprt.
expr | Source expression |
Definition at line 926 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by smt2_convt::convert_expr(), smt2_convt::convert_plus(), and java_bytecode_instrumentt::instrument_expr().
|
inline |
Cast a generic exprt to a plus_exprt.
This is an unchecked conversion. expr must be known to be plus_exprt.
expr | Source expression |
Definition at line 938 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a popcount_exprt.
This is an unchecked conversion. expr must be known to be popcount_exprt.
expr | Source expression |
Definition at line 4918 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by boolbvt::convert_bitvector(), smt2_convt::convert_expr(), and simplify_exprt::simplify_node().
|
inline |
Cast a generic exprt to a popcount_exprt.
This is an unchecked conversion. expr must be known to be popcount_exprt.
expr | Source expression |
Definition at line 4928 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a power_exprt.
This is an unchecked conversion. expr must be known to be power_exprt.
expr | Source expression |
Definition at line 1266 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a power_exprt.
This is an unchecked conversion. expr must be known to be power_exprt.
expr | Source expression |
Definition at line 1276 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a quantifier_exprt.
This is an unchecked conversion. expr must be known to be quantifier_exprt.
expr | Source expression |
Definition at line 4830 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
Referenced by format_rec().
|
inline |
Cast a generic exprt to a quantifier_exprt.
This is an unchecked conversion. expr must be known to be quantifier_exprt.
expr | Source expression |
Definition at line 4840 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
Cast a generic exprt to a rem_exprt.
This is an unchecked conversion. expr must be known to be rem_exprt.
expr | Source expression |
Definition at line 1212 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Cast a generic exprt to a rem_exprt.
This is an unchecked conversion. expr must be known to be rem_exprt.
expr | Source expression |
Definition at line 1222 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a replication_exprt.
This is an unchecked conversion. expr must be known to be replication_exprt.
expr | Source expression |
Definition at line 2958 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by boolbvt::convert_bitvector().
|
inline |
Cast a generic exprt to a replication_exprt.
This is an unchecked conversion. expr must be known to be replication_exprt.
expr | Source expression |
Definition at line 2970 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a shift_exprt.
This is an unchecked conversion. expr must be known to be shift_exprt.
expr | Source expression |
Definition at line 2818 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
Referenced by goto_checkt::check_rec(), boolbvt::convert_bitvector(), bv_pointerst::convert_pointer_type(), rw_range_sett::get_objects_rec(), and c_typecheck_baset::typecheck_expr_main().
|
inline |
Cast a generic exprt to a shift_exprt.
This is an unchecked conversion. expr must be known to be shift_exprt.
expr | Source expression |
Definition at line 2829 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
|
inline |
Cast a generic exprt to a struct_exprt.
This is an unchecked conversion. expr must be known to be struct_exprt.
expr | Source expression |
Definition at line 1838 of file std_expr.h.
References irept::id(), and PRECONDITION.
Referenced by string_constraint_generatort::add_axioms_for_format(), boolbvt::convert_bitvector(), smt2_convt::convert_expr(), java_object_factoryt::gen_nondet_struct_init(), rw_range_sett::get_objects_rec(), java_static_lifetime_init(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), set_class_identifier(), and remove_const_function_pointerst::try_resolve_member().
|
inline |
Cast a generic exprt to a struct_exprt.
This is an unchecked conversion. expr must be known to be struct_exprt.
expr | Source expression |
Definition at line 1847 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a symbol_exprt.
This is an unchecked conversion. expr must be known to be symbol_exprt.
expr | Source expression |
Definition at line 210 of file std_expr.h.
References DATA_INVARIANT, exprt::has_operands(), irept::id(), and PRECONDITION.
Referenced by actuals_replace_map(), uninitializedt::add_assertions(), aliasing(), template_mapt::apply(), value_sett::apply_code_rec(), code_contractst::apply_contract(), cpp_typecheck_resolvet::apply_template_args(), array_name(), uninitialized_domaint::assign(), local_may_aliast::assign_lhs(), local_bitvector_analysist::assign_lhs(), global_may_alias_domaint::assign_lhs_aliases(), escape_domaint::assign_lhs_aliases(), escape_domaint::assign_lhs_cleanup(), constant_propagator_domaint::assign_rec(), value_set_fit::assign_rec(), value_set_fivrnst::assign_rec(), value_sett::assign_rec(), interval_domaint::assume_rec(), boolbvt::boolbv_set_equality_to_true(), localst::build(), local_may_aliast::build(), string_abstractiont::build(), build_ssa_identifier_rec(), inv_object_storet::build_string(), mm2cppt::check_acyclic(), check_and_replace_target(), escape_domaint::check_lhs(), goto_convertt::clean_expr(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), goto_program2codet::cleanup_function_call(), dump_ct::cleanup_harness(), concurrency_instrumentationt::collect(), goto_checkt::collect_allocations(), compute_address_taken_functions(), cfg_baset< cfg_nodet >::compute_edges_function_call(), compute_functions(), rw_set_functiont::compute_rec(), boolbvt::convert_bitvector(), prop_conv_solvert::convert_bool(), jsil_convertt::convert_code(), expr2ct::convert_code_decl(), convert_decl(), goto_program2codet::convert_decl(), goto_convertt::convert_decl(), smt2_convt::convert_expr(), smt2_convt::convert_floatbv(), java_bytecode_convert_methodt::convert_iinc(), boolbvt::convert_index(), java_bytecode_convert_methodt::convert_instructions(), bv_pointerst::convert_pointer_type(), java_bytecode_convert_methodt::convert_store(), smt2_solvert::define_constants(), string_instrumentationt::do_function_call(), goto_convertt::do_function_call(), flow_insensitive_analysis_baset::do_function_call_rec(), static_analysis_baset::do_function_call_rec(), ai_baset::do_function_call_rec(), parameter_assignmentst::do_function_calls(), remove_returnst::do_function_calls(), c_typecheck_baset::do_special_functions(), interpretert::evaluate_address(), interpretert::execute_function_call(), goto_inlinet::expand_function_call(), dirtyt::find_dirty_address_of(), require_goto_statements::find_function_calls(), find_macros(), require_goto_statements::find_pointer_assignments(), find_symbols(), smt2_convt::find_symbols(), require_goto_statements::find_this_component_assignment(), find_used_functions(), remove_function_pointerst::fix_return_type(), namespace_baset::follow_macros(), forall_callsites(), format_rec(), polynomialt::from_expr(), remove_exceptionst::function_or_callees_may_throw(), ci_lazy_methodst::gather_needed_globals(), gather_symbol_live_ranges(), smt2_convt::get(), prop_conv_solvert::get_bool(), remove_virtual_functionst::get_child_functions_rec(), goto_convertt::get_constant(), goto_programt::get_decl_identifiers(), escape_domaint::get_function(), get_function_name(), code_declt::get_identifier(), code_deadt::get_identifier(), function_modifiest::get_modifies_function(), ssa_exprt::get_object_name(), get_objects_rec(), rw_range_sett::get_objects_rec(), local_bitvector_analysist::get_rec(), global_may_alias_domaint::get_rhs_aliases(), escape_domaint::get_rhs_aliases(), global_may_alias_domaint::get_rhs_aliases_address_of(), escape_domaint::get_rhs_aliases_address_of(), escape_domaint::get_rhs_cleanup(), symex_slicet::get_symbols(), uninitializedt::get_tracking(), value_set_fit::get_value_set_rec(), value_set_fivrnst::get_value_set_rec(), value_sett::get_value_set_rec(), goto_checkt::goto_check(), goto_partial_inline(), cpp_typecheck_resolvet::guess_function_template_args(), symex_dereference_statet::has_failed_symbol(), goto_program_dereferencet::has_failed_symbol(), has_symbol(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), interval_domaint::havoc_rec(), implicit(), symex_slice_by_tracet::implied_guards(), mm2cppt::instruction2cpp(), taint_analysist::instrument(), concurrency_instrumentationt::instrument(), cover_cover_instrumentert::instrument(), remove_exceptionst::instrument_function_call(), instrument_preconditions(), goto_checkt::invalidate(), constant_propagator_domaint::valuest::is_constant(), pointer_logict::is_dynamic_object(), is_fence(), is_lwfence(), is_nondet_returning_object(), remove_calls_no_bodyt::is_opaque_function_call(), is_symbol_with_id(), is_typecast_with_id(), acceleratet::is_underapproximate(), postconditiont::is_used(), json(), link_functions(), linker_script_merget::linker_script_merget(), list_calls_and_arguments(), prop_conv_solvert::literal(), mm_io(), model_argc_argv(), nondet_static(), custom_bitvector_domaint::object2id(), simplify_exprt::objects_equal_address_of(), full_slicert::operator()(), check_call_sequencet::operator()(), goto_symex_statet::propagationt::operator()(), local_may_aliast::output(), print_global_state_size(), _rw_set_loct::read_write_rec(), references_class_model(), cpp_typecheck_resolvet::remove_duplicates(), goto_convertt::remove_function_call(), graphml_witnesst::remove_l0_l1(), rename_symbolt::rename(), goto_symex_statet::rename(), replace_symbolt::replace(), character_refine_preprocesst::replace_character_call(), remove_const_function_pointerst::replace_const_symbols(), require_goto_statements::require_entry_point_argument_assignment(), require_goto_statements::require_struct_array_component_assignment(), require_goto_statements::require_struct_component_assignment(), require_expr::require_symbol(), remove_returnst::restore_returns(), goto_symext::rewrite_quantifiers(), java_bytecode_convert_methodt::save_stack_entries(), prop_conv_solvert::set_equality_to_true(), smt2_convt::set_to(), show_call_sequences(), cpp_typecheck_resolvet::show_identifiers(), simplify_exprt::simplify_dynamic_object(), simplify_exprt::simplify_inequality_address_of(), slice_global_inits(), acceleration_utilst::stash_variables(), polynomial_acceleratort::stash_variables(), polynomialt::substitute(), member_exprt::symbol(), linker_script_merget::symbols_to_pointerize(), goto_symext::symex_assign(), goto_symext::symex_assign_symbol(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_function_call_code(), goto_symext::symex_function_call_symbol(), thread_exit_instrumentation(), jsil_declarationt::to_symbol(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), uncaught_exceptions_domaint::transform(), escape_domaint::transform(), rd_range_domaint::transform_dead(), rd_range_domaint::transform_function_call(), remove_const_function_pointerst::try_resolve_function_call(), type2name(), java_bytecode_typecheckt::typecheck_expr(), jsil_typecheckt::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_symbol(), jsil_typecheckt::typecheck_function_call(), c_typecheck_baset::typecheck_side_effect_function_call(), undefined_function_abort_path(), remove_returnst::undo_function_calls(), jsil_typecheckt::update_expr_type(), value_set_dereferencet::valid_check(), instrumentert::cfg_visitort::visit_cfg_function_call(), shared_bufferst::cfg_visitort::weak_memory(), and yyjsilparse().
|
inline |
Cast a generic exprt to a symbol_exprt.
This is an unchecked conversion. expr must be known to be symbol_exprt.
expr | Source expression |
Definition at line 220 of file std_expr.h.
References DATA_INVARIANT, exprt::has_operands(), irept::id(), and PRECONDITION.
Cast a generic exprt to a transt.
This is an unchecked conversion. expr must be known to be transt.
expr | Source expression |
Definition at line 57 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Definition at line 69 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a typecast_exprt.
This is an unchecked conversion. expr must be known to be typecast_exprt.
expr | Source expression |
Definition at line 2143 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by adjust_float_expressions(), custom_bitvector_analysist::aliases(), local_may_aliast::assign_lhs(), local_bitvector_analysist::assign_lhs(), value_set_fit::assign_rec(), value_set_fivrnst::assign_rec(), value_set_fivrt::assign_rec(), value_sett::assign_rec(), interval_domaint::assume_rec(), string_abstractiont::build(), build_full_lhs_rec(), build_object_descriptor_rec(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), goto_symex_statet::constant_propagation(), boolbvt::convert_bitvector(), smt2_convt::convert_expr(), boolbvt::convert_rest(), expr2ct::convert_with_precedence(), dereferencet::dereference_rec(), goto_symext::dereference_rec(), format_rec(), custom_bitvector_analysist::get_bit_nr(), escape_domaint::get_function(), rw_range_sett::get_objects_address_of(), rw_range_sett::get_objects_rec(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), custom_bitvector_domaint::get_rhs(), global_may_alias_domaint::get_rhs_aliases(), escape_domaint::get_rhs_aliases(), escape_domaint::get_rhs_cleanup(), get_symbol(), have_to_adjust_float_expressions(), have_to_remove_complex(), interval_domaint::havoc_rec(), goto_symext::havoc_rec(), is_skip(), is_typecast_with_id(), make_va_list(), custom_bitvector_domaint::object2id(), require_goto_statements::require_struct_array_component_assignment(), require_goto_statements::require_struct_component_assignment(), require_expr::require_typecast(), java_bytecode_convert_methodt::save_stack_entries(), goto_program2codet::scan_for_varargs(), skip_typecast(), goto_symext::symex_assign_rec(), remove_const_function_pointerst::try_resolve_expression(), and remove_const_function_pointerst::try_resolve_function_call().
|
inline |
Cast a generic exprt to a typecast_exprt.
This is an unchecked conversion. expr must be known to be typecast_exprt.
expr | Source expression |
Definition at line 2155 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a unary_exprt.
This is an unchecked conversion. expr must be known to be unary_exprt.
expr | Source expression |
Definition at line 361 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
Referenced by boolbvt::convert_bitvector(), boolbvt::convert_rest(), and format_rec().
|
inline |
Cast a generic exprt to a unary_exprt.
This is an unchecked conversion. expr must be known to be unary_exprt.
expr | Source expression |
Definition at line 372 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
|
inline |
Cast a generic exprt to a unary_minus_exprt.
This is an unchecked conversion. expr must be known to be unary_minus_exprt.
expr | Source expression |
Definition at line 474 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by float_bvt::convert().
|
inline |
Cast a generic exprt to a unary_minus_exprt.
This is an unchecked conversion. expr must be known to be unary_minus_exprt.
expr | Source expression |
Definition at line 486 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a union_exprt.
This is an unchecked conversion. expr must be known to be union_exprt.
expr | Source expression |
Definition at line 1782 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), boolbvt::convert_bitvector(), smt2_convt::convert_expr(), simplify_exprt::expr2bits(), json(), rewrite_union(), simplify_exprt::simplify_member(), and xml().
|
inline |
Cast a generic exprt to a union_exprt.
This is an unchecked conversion. expr must be known to be union_exprt.
expr | Source expression |
Definition at line 1794 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an update_exprt.
This is an unchecked conversion. expr must be known to be update_exprt.
expr | Source expression |
Definition at line 3741 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by arrayst::add_array_constraints(), arrayst::collect_arrays(), simplify_exprt::simplify_member(), and simplify_exprt::simplify_update().
|
inline |
Cast a generic exprt to an update_exprt.
This is an unchecked conversion. expr must be known to be update_exprt.
expr | Source expression |
Definition at line 3753 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to an vector_exprt.
This is an unchecked conversion. expr must be known to be vector_exprt.
expr | Source expression |
Definition at line 1707 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to an vector_exprt.
This is an unchecked conversion. expr must be known to be vector_exprt.
expr | Source expression |
Definition at line 1716 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Cast a generic exprt to a with_exprt.
This is an unchecked conversion. expr must be known to be with_exprt.
expr | Source expression |
Definition at line 3519 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by arrayst::add_array_constraints(), arrayst::collect_arrays(), smt2_convt::convert_expr(), interpretert::evaluate(), make_with_expr(), goto_symex_statet::rename(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_member(), and smt2_convt::use_array_theory().
|
inline |
Cast a generic exprt to a with_exprt.
This is an unchecked conversion. expr must be known to be with_exprt.
expr | Source expression |
Definition at line 3531 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Cast a generic exprt to a xor_exprt.
This is an unchecked conversion. expr must be known to be xor_exprt.
expr | Source expression |
Definition at line 2498 of file std_expr.h.
References irept::id(), and PRECONDITION.
Cast a generic exprt to a bitxor_exprt.
This is an unchecked conversion. expr must be known to be bitxor_exprt.
expr | Source expression |
Definition at line 2507 of file std_expr.h.
References irept::id(), and PRECONDITION.
|
inline |
Definition at line 82 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 231 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 295 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 436 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 499 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 568 of file std_expr.h.
References DATA_INVARIANT, unary_exprt::op(), exprt::type(), and validate_operands().
|
inline |
Definition at line 951 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 1009 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 1067 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 1125 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 1179 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 1233 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 1287 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 1346 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 1398 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 1454 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 1542 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 1609 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 1677 of file std_expr.h.
References exprt::operands(), and PRECONDITION.
|
inline |
Definition at line 1807 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 1935 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 2027 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 2103 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 2168 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 2247 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 2383 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 2983 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 3064 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 3162 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 3222 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 3276 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 3353 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 3451 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 3544 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 3608 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 3664 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 3766 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 3980 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 4032 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 4088 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 4140 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 4192 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 4249 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 4308 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 4612 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 4776 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 4852 of file std_expr.h.
References validate_operands().
|
inline |
Definition at line 4940 of file std_expr.h.
References validate_operands().