cprover
|
Conversion to subclasses of exprt
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 323 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by float_bvt::convert().
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 335 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 2629 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by const_function_pointer_propagationt::arg_stackt::add_args(), string_constraint_generatort::add_axioms_for_java_char_array(), 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(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), dirtyt::find_dirty(), custom_bitvector_analysist::get_bit_nr(), escape_domaint::get_function(), rw_range_sett::get_objects_rec(), get_old_va_symbol(), 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(), custom_bitvector_domaint::object2id(), goto_symext::process_array_expr(), goto_symext::process_array_expr_rec(), const_function_pointer_propagationt::propagate(), replace_symbol_extt::replace(), replace_async(), simplify_exprt::simplify_dereference(), 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 2639 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 1903 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 1915 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 1332 of file std_expr.h.
References irept::id(), and PRECONDITION.
Referenced by string_abstractiont::build(), dplib_convt::convert_dplib_expr(), cvc_convt::convert_expr(), 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 1341 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 1286 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by arrayst::add_array_constraints(), boolbvt::convert_bitvector(), and path_symext::propagate().
|
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 1298 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 524 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
Referenced by boolbvt::convert_bitvector().
|
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 535 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 619 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 630 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 2204 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 2216 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 2065 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 2076 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 2111 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 2123 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 2157 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 2169 of file std_expr.h.
References irept::id(), 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 1553 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 1565 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 3885 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 3897 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 3725 of file std_expr.h.
References irept::id(), and PRECONDITION.
Referenced by interval_domaint::assume_rec(), build_ssa_identifier_rec(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), goto_program2codet::convert_assign_varargs(), boolbvt::convert_bitvector(), expr2ct::convert_constant(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), java_bytecode_convert_methodt::convert_instructions(), bv_pointerst::convert_pointer_type(), smt2_convt::convert_rounding_mode_FPA(), 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(), 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(), unsignedbv_typet::largest_expr(), signedbv_typet::largest_expr(), exprt::mul(), exprt::negate(), format_constantt::operator()(), smt2_convt::parse_struct(), simplify_exprt::simplify_abs(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_div(), 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_exprt::simplify_sign(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_unary_minus(), unsignedbv_typet::smallest_expr(), signedbv_typet::smallest_expr(), string_refinementt::string_of_array(), exprt::sum(), string_refinementt::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(), java_bytecode_convert_methodt::variable(), xml(), unsignedbv_typet::zero_expr(), and signedbv_typet::zero_expr().
|
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 3734 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 2748 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(), path_symex_statet::dereference_rec(), dirtyt::find_dirty_address_of(), function_modifiest::get_modifies_lhs(), get_modifies_lhs(), get_objects_rec(), rw_range_sett::get_objects_rec(), path_symex_statet::instantiate_rec_address(), constant_propagator_domaint::valuest::is_constant_address_of(), mm_io(), nondet_volatile_lhs(), custom_bitvector_domaint::object2id(), const_function_pointer_propagationt::propagate(), 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 2760 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 879 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by goto_checkt::check_rec(), boolbvt::convert_bitvector(), smt1_convt::convert_expr(), 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 891 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 1701 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by value_sett::assign_rec(), value_set_fit::assign_rec(), value_set_fivrnst::assign_rec(), value_set_fivrt::assign_rec(), value_sett::do_free(), value_set_fit::do_free(), value_set_fivrnst::do_free(), value_set_fivrt::do_free(), value_sett::get_value_set_rec(), value_set_fit::get_value_set_rec(), value_set_fivrnst::get_value_set_rec(), and value_set_fivrt::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 1714 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 1105 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(), boolbvt::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 1115 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 2482 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by boolbvt::convert_rest().
|
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 2494 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 2570 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 an extractbits_exprt.
This is an unchecked conversion. expr must be known to be extractbits_exprt.
expr | Source expression |
Definition at line 2582 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 1071 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 1059 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 1829 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 1841 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 3826 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by string_constraint_generatort::add_axioms_for_string_expr(), boolbvt::convert_bitvector(), string_refinementt::convert_rest(), and expr2ct::convert_with_precedence().
|
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 3839 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 3520 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 3532 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 3567 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 3580 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 3650 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 3661 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 2836 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by arrayst::add_array_constraints(), string_constraint_generatort::add_axioms_for_string_expr(), goto_symext::address_arithmetic(), local_may_aliast::assign_lhs(), local_bitvector_analysist::assign_lhs(), path_symext::assign_rec(), 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(), dirtyt::find_dirty_address_of(), bdd_exprt::from_expr_rec(), path_symext::function_call_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(), interval_domaint::havoc_rec(), path_symex_statet::instantiate_rec_address(), goto_symext::is_index_member_symbol_if(), lift_if(), nondet_volatile_lhs(), goto_symext::process_array_expr(), goto_symext::process_array_expr_rec(), path_symext::propagate(), 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 2848 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 1949 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 1959 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 2970 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 2982 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 1229 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(), path_symex_statet::array_theory(), uninitialized_domaint::assign(), local_may_aliast::assign_lhs(), local_bitvector_analysist::assign_lhs(), 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(), goto_symex_statet::constant_propagation_reference(), bv_pointerst::convert_address_of_rec(), smt1_convt::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), boolbvt::convert_bitvector(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), bv_pointerst::convert_pointer_type(), boolbvt::convert_rest(), smt1_convt::convert_with(), expr2ct::convert_with_precedence(), goto_symext::dereference_rec(), goto_symext::dereference_rec_address_of(), dirtyt::find_dirty_address_of(), acceleration_utilst::gather_array_assignments(), smt1_convt::get(), 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_checkt::invalidate(), constant_propagator_domaint::valuest::is_constant_address_of(), goto_symext::is_index_member_symbol_if(), is_lvalue(), path_symex_statet::is_symbol_member_index(), boolbvt::literal(), goto_convertt::needs_cleaning(), nondet_volatile_lhs(), find_index_visitort::operator()(), goto_symext::process_array_expr(), goto_symext::process_array_expr_rec(), pointer_arithmetict::read(), dereferencet::read_object(), path_symex_statet::read_symbol_member_index(), goto_symex_statet::rename_address(), rewrite_assignment(), simplify_exprt::simplify_address_of(), simplify_exprt::simplify_dereference(), simplify_exprt::simplify_index(), simplify_exprt::simplify_inequality_address_of(), 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 1241 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 3436 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 3446 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 3390 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 3402 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 3348 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 3358 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 3478 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 3488 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 3969 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by smt2_convt::convert_expr().
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 3979 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Cast a generic exprt to a literal_exprt.
This is an unchecked conversion. expr must be known to be literal_exprt.
expr | Source expression |
Definition at line 49 of file literal_expr.h.
References exprt::has_operands(), and irept::id().
Referenced by cvc_convt::convert(), smt1_convt::convert(), smt2_convt::convert(), prop_conv_solvert::convert_bool(), smt1_convt::convert_expr(), and smt2_convt::convert_expr().
|
inline |
Cast a generic exprt to a literal_exprt.
This is an unchecked conversion. expr must be known to be literal_exprt.
expr | Source expression |
Definition at line 58 of file literal_expr.h.
References exprt::has_operands(), and irept::id().
|
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 3016 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 3028 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 3302 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(), path_symext::assign_rec(), string_abstractiont::build(), build_full_lhs_rec(), build_object_descriptor_rec(), build_ssa_identifier_rec(), goto_checkt::check_rec(), arrayst::collect_arrays(), dplib_convt::convert_address_of_rec(), cvc_convt::convert_address_of_rec(), bv_pointerst::convert_address_of_rec(), smt1_convt::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), graphml_witnesst::convert_assign_rec(), boolbvt::convert_bitvector(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), smt1_convt::convert_member(), smt2_convt::convert_member(), bv_pointerst::convert_pointer_type(), boolbvt::convert_rest(), smt1_convt::convert_with(), expr2ct::convert_with_precedence(), goto_symext::dereference_rec_address_of(), interpretert::evaluate_address(), dirtyt::find_dirty_address_of(), smt1_convt::get(), smt2_convt::get(), rw_range_sett::get_objects_address_of(), get_objects_rec(), rw_range_sett::get_objects_rec(), have_to_rewrite_union(), path_symex_statet::instantiate_rec(), path_symex_statet::instantiate_rec_address(), goto_checkt::invalidate(), constant_propagator_domaint::valuest::is_constant_address_of(), goto_symext::is_index_member_symbol_if(), is_lvalue(), path_symex_statet::is_symbol_member_index(), boolbvt::literal(), nondet_volatile_lhs(), path_symext::propagate(), dereferencet::read_object(), path_symex_statet::read_symbol_member_index(), goto_symex_statet::rename_address(), rewrite_assignment(), rewrite_union(), java_bytecode_convert_methodt::save_stack_entries(), simplify_exprt::simplify_address_of_arg(), 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 3314 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 783 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by smt1_convt::convert_expr(), and 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 795 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 927 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by goto_checkt::check_rec(), boolbvt::convert_bitvector(), smt1_convt::convert_expr(), 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 937 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 831 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by smt1_convt::convert_expr(), and 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 843 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 687 of file std_expr.h.
|
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 695 of file std_expr.h.
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 2682 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 2692 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 1147 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 1159 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 1634 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 1647 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 2019 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 2031 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 735 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by smt1_convt::convert_expr(), smt2_convt::convert_expr(), and smt2_convt::convert_plus().
|
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 747 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 1015 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 1025 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 971 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 981 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 2411 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 2423 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 2280 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 2291 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
Cast a generic exprt to an ssa_exprt.
This is an unchecked conversion. expr must be known to be ssa_exprt.
expr | Source expression |
Definition at line 150 of file ssa_expr.h.
References irept::get_bool(), exprt::has_operands(), and irept::id().
Referenced by string_constraint_generatort::add_axioms_for_function_application(), goto_symext::address_arithmetic(), array_name(), check_renaming(), check_renaming_l1(), compute_pointer_offset(), goto_symex_statet::get_l1_name(), goto_symex_statet::get_original_name(), get_symbol(), symex_dereference_statet::has_failed_symbol(), postconditiont::is_used(), goto_symex_statet::l2_thread_read_encoding(), goto_symext::phi_function(), goto_symext::process_array_expr(), goto_symext::process_array_expr_rec(), graphml_witnesst::remove_l0_l1(), goto_symex_statet::rename(), goto_symex_statet::rename_address(), goto_symext::rewrite_quantifiers(), goto_symext::symex_assign_rec(), goto_symext::symex_dead(), goto_symext::trigger_auto_object(), and value_set_dereferencet::valid_check().
Cast a generic exprt to an ssa_exprt.
This is an unchecked conversion. expr must be known to be ssa_exprt.
expr | Source expression |
Definition at line 161 of file ssa_expr.h.
References irept::get_bool(), exprt::has_operands(), and irept::id().
|
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 1487 of file std_expr.h.
References irept::id(), and PRECONDITION.
Referenced by boolbvt::convert_bitvector(), smt2_convt::convert_expr(), goto_convertt::do_java_new(), rw_range_sett::get_objects_rec(), 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 1496 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 202 of file std_expr.h.
References DATA_INVARIANT, exprt::has_operands(), irept::id(), and PRECONDITION.
Referenced by call_grapht::add(), const_function_pointer_propagationt::arg_stackt::add_args(), uninitializedt::add_assertions(), string_constraint_generatort::add_axioms_for_function_application(), string_constraint_generatort::add_axioms_for_string_expr(), string_constraint_generatort::add_axioms_from_literal(), aliasing(), value_sett::apply_code(), code_contractst::apply_contract(), 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(), path_symext::assign_rec(), constant_propagator_domaint::assign_rec(), value_sett::assign_rec(), interval_domaint::assume_rec(), string_refinementt::boolbv_set_equality_to_true(), boolbvt::boolbv_set_equality_to_true(), localst::build(), local_may_aliast::build(), string_abstractiont::build(), build_ssa_identifier_rec(), escape_domaint::check_lhs(), goto_convertt::clean_expr(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), goto_program2codet::cleanup_function_call(), 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(), goto_program2codet::convert_decl(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), smt2_convt::convert_floatbv(), boolbvt::convert_index(), java_bytecode_convert_methodt::convert_instructions(), bv_pointerst::convert_pointer_type(), string_refinementt::convert_symbol(), string_instrumentationt::do_function_call(), goto_convertt::do_function_call(), parameter_assignmentst::do_function_calls(), remove_returnst::do_function_calls(), c_typecheck_baset::do_special_functions(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), goto_inlinet::expand_function_call(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), dirtyt::find_dirty_address_of(), find_symbols(), smt1_convt::find_symbols(), smt2_convt::find_symbols(), polynomialt::from_expr(), path_symext::function_call_rec(), gather_needed_globals(), gather_symbol_live_ranges(), smt1_convt::get(), smt2_convt::get(), prop_conv_solvert::get_bool(), goto_inlinet::get_call(), remove_virtual_functionst::get_child_functions_rec(), goto_convertt::get_constant(), goto_programt::get_decl_identifiers(), escape_domaint::get_function(), remove_virtual_functionst::get_functions(), 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(), get_old_va_symbol(), 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_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(), interval_domaint::havoc_rec(), implicit(), taint_analysist::instrument(), concurrency_instrumentationt::instrument(), instrument_cover_goals(), remove_exceptionst::instrument_function_call(), goto_checkt::invalidate(), constant_propagator_domaint::valuest::is_array_constant(), constant_propagator_domaint::valuest::is_constant(), pointer_logict::is_dynamic_object(), acceleratet::is_underapproximate(), link_functions(), list_calls_and_arguments(), prop_conv_solvert::literal(), mm_io(), nondet_static(), custom_bitvector_domaint::object2id(), full_slicert::operator()(), check_call_sequencet::operator()(), const_function_pointer_propagationt::propagate(), path_symex_statet::read_symbol_member_index(), _rw_set_loct::read_write_rec(), graphml_witnesst::remove_l0_l1(), rename_symbolt::rename(), goto_symex_statet::rename(), replace_async(), character_refine_preprocesst::replace_character_call(), remove_returnst::restore_returns(), goto_symext::rewrite_quantifiers(), java_bytecode_convert_methodt::save_stack_entries(), prop_conv_solvert::set_equality_to_true(), string_constraint_generatort::set_string_symbol_equal_to_expr(), smt2_convt::set_to(), show_call_sequences(), cpp_typecheck_resolvet::show_identifiers(), simplify_exprt::simplify_dynamic_object(), slice_global_inits(), acceleration_utilst::stash_variables(), polynomial_acceleratort::stash_variables(), polynomialt::substitute(), goto_symext::symex_assign(), 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(), escape_domaint::transform(), rd_range_domaint::transform_dead(), rd_range_domaint::transform_function_call(), 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(), string_constraintt::univ_var(), 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 212 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 59 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Definition at line 71 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 1760 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.
Referenced by string_constraint_generatort::add_axioms_for_string_expr(), adjust_float_expressions(), custom_bitvector_analysist::aliases(), local_may_aliast::assign_lhs(), local_bitvector_analysist::assign_lhs(), path_symext::assign_rec(), value_sett::assign_rec(), value_set_fit::assign_rec(), value_set_fivrnst::assign_rec(), value_set_fivrt::assign_rec(), interval_domaint::assume_rec(), string_refinementt::boolbv_set_equality_to_true(), 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(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), boolbvt::convert_rest(), expr2ct::convert_with_precedence(), dereferencet::dereference_rec(), goto_symext::dereference_rec(), path_symext::function_call_rec(), smt1_convt::get(), custom_bitvector_analysist::get_bit_nr(), escape_domaint::get_function(), rw_range_sett::get_objects_address_of(), rw_range_sett::get_objects_rec(), get_old_va_symbol(), 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(), is_skip(), make_va_list(), custom_bitvector_domaint::object2id(), goto_symext::process_array_expr(), goto_symext::process_array_expr_rec(), path_symext::propagate(), 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 1772 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 279 of file std_expr.h.
References DATA_INVARIANT, and exprt::operands().
Referenced by boolbvt::convert_bitvector(), and boolbvt::convert_rest().
|
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 290 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 376 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 388 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 1441 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(), path_symext::propagate(), 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 1453 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 3108 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 3120 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 1372 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 1381 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 2919 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(), 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 2931 of file std_expr.h.
References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.