cprover
|
#include "arith_tools.h"
#include "fixedbv.h"
#include "ieee_float.h"
#include "invariant.h"
#include "std_types.h"
#include "std_expr.h"
Go to the source code of this file.
Functions | |
bool | to_integer (const exprt &expr, mp_integer &int_value) |
bool | to_integer (const constant_exprt &expr, mp_integer &int_value) |
bool | to_unsigned_integer (const constant_exprt &expr, unsigned &uint_value) |
convert a positive integer expression to an unsigned int More... | |
constant_exprt | from_integer (const mp_integer &int_value, const typet &type) |
std::size_t | address_bits (const mp_integer &size) |
ceil(log2(size)) More... | |
mp_integer | power (const mp_integer &base, const mp_integer &exponent) |
A multi-precision implementation of the power operator. More... | |
void | mp_min (mp_integer &a, const mp_integer &b) |
void | mp_max (mp_integer &a, const mp_integer &b) |
std::size_t address_bits | ( | const mp_integer & | size | ) |
ceil(log2(size))
Definition at line 210 of file arith_tools.cpp.
References INVARIANT, and power().
Referenced by partial_order_concurrencyt::build_clock_type(), build_sizeof_expr(), boolbvt::convert_extractbit(), float_bvt::from_signed_integer(), float_utilst::from_signed_integer(), float_bvt::from_unsigned_integer(), float_utilst::from_unsigned_integer(), boolbv_widtht::get_entry(), float_bvt::limit_distance(), float_utilst::limit_distance(), lower_popcount(), float_bvt::normalization_shift(), float_utilst::normalization_shift(), float_bvt::rounder(), and float_utilst::rounder().
constant_exprt from_integer | ( | const mp_integer & | int_value, |
const typet & | type | ||
) |
Definition at line 108 of file arith_tools.cpp.
References fixedbvt::from_integer(), ieee_floatt::from_integer(), irept::get_size_t(), bitvector_typet::get_width(), irept::id(), integer2binary(), integer2string(), PRECONDITION, r, constant_exprt::set_value(), fixedbvt::spec, typet::subtype(), to_bv_type(), to_c_bit_field_type(), to_c_bool_type(), to_c_enum_type(), fixedbvt::to_expr(), ieee_floatt::to_expr(), to_fixedbv_type(), to_floatbv_type(), to_pointer_type(), to_signedbv_type(), and to_unsignedbv_type().
Referenced by string_abstractiont::abstract_char_assign(), string_abstractiont::abstract_function_call(), disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), c_typecheck_baset::add_argc_argv(), string_constraint_generatort::add_axioms_for_char_literal(), string_constraint_generatort::add_axioms_for_characters_in_integer_string(), string_constraint_generatort::add_axioms_for_code_point(), string_constraint_generatort::add_axioms_for_code_point_at(), string_constraint_generatort::add_axioms_for_code_point_before(), string_constraint_generatort::add_axioms_for_code_point_count(), string_constraint_generatort::add_axioms_for_compare_to(), string_constraint_generatort::add_axioms_for_concat(), string_constraint_generatort::add_axioms_for_concat_char(), string_constraint_generatort::add_axioms_for_concat_substr(), string_constraint_generatort::add_axioms_for_constant(), string_constraint_generatort::add_axioms_for_constrain_characters(), string_constraint_generatort::add_axioms_for_contains(), string_constraint_generatort::add_axioms_for_copy(), string_constraint_generatort::add_axioms_for_correct_number_format(), string_constraint_generatort::add_axioms_for_cprover_string(), string_constraint_generatort::add_axioms_for_delete(), string_constraint_generatort::add_axioms_for_delete_char_at(), string_constraint_generatort::add_axioms_for_empty_string(), string_constraint_generatort::add_axioms_for_equals(), string_constraint_generatort::add_axioms_for_equals_ignore_case(), string_constraint_generatort::add_axioms_for_format(), string_constraint_generatort::add_axioms_for_fractional_part(), string_constraint_generatort::add_axioms_for_index_of(), string_constraint_generatort::add_axioms_for_index_of_string(), string_constraint_generatort::add_axioms_for_insert(), string_constraint_generatort::add_axioms_for_is_prefix(), string_constraint_generatort::add_axioms_for_is_suffix(), string_constraint_generatort::add_axioms_for_last_index_of(), string_constraint_generatort::add_axioms_for_last_index_of_string(), string_constraint_generatort::add_axioms_for_parse_int(), string_constraint_generatort::add_axioms_for_replace(), string_constraint_generatort::add_axioms_for_set_char(), string_constraint_generatort::add_axioms_for_set_length(), string_constraint_generatort::add_axioms_for_string_of_float(), string_constraint_generatort::add_axioms_for_string_of_int(), string_constraint_generatort::add_axioms_for_string_of_int_with_radix(), string_constraint_generatort::add_axioms_for_substring(), string_constraint_generatort::add_axioms_for_to_lower_case(), string_constraint_generatort::add_axioms_for_to_upper_case(), string_constraint_generatort::add_axioms_for_trim(), string_constraint_generatort::add_axioms_from_bool(), string_constraint_generatort::add_axioms_from_char(), string_constraint_generatort::add_axioms_from_float_scientific_notation(), float_bvt::add_bias(), string_constraint_generatort::add_constraint_on_characters(), string_refinementt::add_lemma(), c_typecheck_baset::add_rounding_mode(), add_stack_depth_symbol(), float_bvt::add_sub(), goto_symext::address_arithmetic(), adjust_float_expressions(), java_object_factoryt::allocate_nondet_length_array(), disjunctive_polynomial_accelerationt::assert_for_values(), polynomial_acceleratort::assert_for_values(), acceleration_utilst::assign_array(), string_constraint_generatort::associate_array_to_pointer(), string_constraint_generatort::associate_length_to_array(), string_exprt< array_string_exprt >::axiom_for_has_length(), string_constraint_generatort::axiom_for_is_positive_index(), string_exprt< array_string_exprt >::axiom_for_length_gt(), string_exprt< array_string_exprt >::axiom_for_length_le(), float_bvt::bias(), goto_checkt::bounds_check(), value_set_dereferencet::bounds_check(), object_descriptor_exprt::build(), value_set_dereferencet::build_reference_to(), build_sizeof_expr(), acceleratet::build_state_machine(), string_abstractiont::build_symbol_constant(), boolbvt::bv_get_unbounded_array(), c_nondet_symbol_factory(), cannot_be_neg(), java_bytecode_instrumentt::check_arithmetic_exception(), java_bytecode_instrumentt::check_array_access(), java_bytecode_instrumentt::check_array_length(), check_axioms(), acceleration_utilst::check_inductive(), polynomial_acceleratort::check_inductive(), goto_program2codet::cleanup_expr(), java_string_library_preprocesst::code_assign_java_string_to_string_expr(), symex_slice_by_tracet::compute_ts_back(), interval_sparse_arrayt::concretize(), interpretert::concretize_type(), constant_bool(), string_constraint_generatort::constant_char(), float_bvt::conversion(), goto_checkt::conversion_check(), smt2_convt::convert_address_of_rec(), graphml_witnesst::convert_assign_rec(), goto_program2codet::convert_assign_rec(), boolbvt::convert_byte_extract(), boolbvt::convert_byte_update(), smt2_convt::convert_byte_update(), convert_character_literal(), java_bytecode_convert_methodt::convert_cmp(), java_bytecode_convert_methodt::convert_cmp2(), character_refine_preprocesst::convert_compare(), java_bytecode_convert_methodt::convert_const(), character_refine_preprocesst::convert_digit_char(), smt2_convt::convert_expr(), boolbvt::convert_extractbit(), convert_float_literal(), character_refine_preprocesst::convert_for_digit(), goto_convertt::convert_gcc_switch_case_range(), java_bytecode_convert_methodt::convert_if(), boolbvt::convert_index(), java_bytecode_convert_methodt::convert_instructions(), convert_integer_literal(), boolbvt::convert_lambda(), boolbvt::convert_member(), smt2_convt::convert_minus(), java_bytecode_convert_methodt::convert_multianewarray(), java_bytecode_convert_methodt::convert_newarray(), smt2_convt::convert_plus(), java_bytecode_convert_methodt::convert_ret(), convert_string_literal(), character_refine_preprocesst::convert_to_code_point(), smt2_convt::convert_typecast(), bv_cbmct::convert_waitfor(), boolbvt::convert_with_array(), boolbvt::convert_with_bv(), copy_array(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), create_clinit_wrapper_symbols(), create_initialize(), float_bvt::denormalization_shift(), DEPRECATED(), dereferencet::dereference_rec(), goto_symext::dereference_rec(), float_bvt::div(), goto_checkt::div_by_zero_check(), acceleration_utilst::do_arrays(), acceleration_utilst::do_assumptions(), string_instrumentationt::do_format_string_read(), string_instrumentationt::do_format_string_write(), c_typecheck_baset::do_initializer_list(), acceleration_utilst::do_nonrecursive(), goto_convertt::do_scanf(), c_typecheck_baset::do_special_functions(), string_instrumentationt::do_strerror(), c_typecastt::do_typecast(), simplify_exprt::eliminate_common_addends(), string_concat_char_builtin_functiont::eval(), string_set_char_builtin_functiont::eval(), string_to_lower_case_builtin_functiont::eval(), string_to_upper_case_builtin_functiont::eval(), string_insertion_builtin_functiont::eval(), string_of_int_builtin_functiont::eval(), value_sett::eval_pointer_offset(), expr_initializert< nondet >::expr_initializer_rec(), character_refine_preprocesst::expr_of_char_count(), character_refine_preprocesst::expr_of_high_surrogate(), character_refine_preprocesst::expr_of_is_bmp_code_point(), character_refine_preprocesst::expr_of_is_defined(), character_refine_preprocesst::expr_of_is_supplementary_code_point(), character_refine_preprocesst::expr_of_is_valid_code_point(), character_refine_preprocesst::expr_of_low_surrogate(), character_refine_preprocesst::expr_of_reverse_bytes(), character_refine_preprocesst::expr_of_to_lower_case(), character_refine_preprocesst::expr_of_to_title_case(), character_refine_preprocesst::expr_of_to_upper_case(), smt2_parsert::expression(), extractbits_exprt::extractbits_exprt(), qbf_bdd_certificatet::f_get(), qbf_squolem_coret::f_get(), smt2_convt::find_symbols(), polynomial_acceleratort::fit_const(), disjunctive_polynomial_accelerationt::fit_polynomial(), smt2_convt::flatten_array(), flatten_byte_extract(), flatten_byte_update(), floatbv_mult(), floatbv_of_int_expr(), float_bvt::fraction_rounding_decision(), float_bvt::from_signed_integer(), float_bvt::from_unsigned_integer(), smt2_parsert::function_application(), function_to_call(), gen_clinit_assign(), gen_clinit_eqexpr(), java_object_factoryt::gen_nondet_array_init(), java_object_factoryt::gen_nondet_struct_init(), generate_ansi_c_start_function(), string_refinementt::get(), float_bvt::rounding_mode_bitst::get(), get_array(), invariant_sett::get_constant(), get_exponent(), get_numeric_value_from_character(), java_string_library_preprocesst::get_object_at_index(), get_or_create_string_literal_symbol(), get_quantifier_var_max(), local_may_aliast::get_rec(), value_set_fivrnst::get_reference_set_rec(), value_sett::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), get_significand(), interpretert::get_size(), get_subexpression_at_offset(), interpretert::get_value(), havoc_generate_function_bodiest::havoc_expr_rec(), character_refine_preprocesst::in_interval_expr(), character_refine_preprocesst::in_list_expr(), initial_index_set(), initialize_nondet_string_fields(), acceleratet::insert_automaton(), instantiate_quantifier(), instrument_get_current_thread_id(), instrument_start_thread(), goto_checkt::integer_overflow_check(), string_instrumentationt::invalidate_buffer(), is_digit_with_radix(), is_lower_case(), is_not_zero(), is_upper_case(), java_build_arguments(), java_record_outputs(), java_root_class_init(), unsignedbv_typet::largest_expr(), signedbv_typet::largest_expr(), string_set_char_builtin_functiont::length_constraint(), string_of_int_builtin_functiont::length_constraint(), length_constraint_for_concat_char(), length_constraint_for_concat_substr(), float_bvt::limit_distance(), remove_java_newt::lower_java_new_array(), lower_popcount(), linker_script_merget::ls_data2instructions(), c_typecheck_baset::make_constant(), java_string_library_preprocesst::make_equals_function_code(), interval_domaint::make_expression(), java_string_library_preprocesst::make_nondet_string_expr(), java_string_library_preprocesst::make_object_get_class_code(), make_string(), member_offset_expr(), value_set_dereferencet::memory_model_bytes(), value_set_dereferencet::memory_model_conversion(), goto_checkt::mod_by_zero_check(), float_bvt::mul(), goto_checkt::nan_check(), negation_of_not_contains_constraint(), invariant_sett::nnf(), float_bvt::normalization_shift(), object_lower_bound(), pointer_logict::object_rec(), dereferencet::operator()(), string_exprt< array_string_exprt >::operator[](), overflow_instrumentert::overflow_expr(), float_bvt::pack(), pair_value(), goto_symext::parameter_assignments(), smt2_convt::parse_literal(), constant_propagator_domaint::partial_evaluate_with_all_rounding_modes(), pointer_logict::pointer_expr(), goto_symext::process_array_expr(), java_bytecode_parsert::rbytecode(), java_bytecode_parsert::rconstant_pool(), pointer_arithmetict::read(), dereferencet::read_object(), record_function_outputs(), remove_complex(), goto_convertt::remove_post(), goto_convertt::remove_pre(), remove_vector(), rewrite_union(), float_bvt::round_exponent(), round_expr_to_zero(), float_bvt::round_fraction(), dynamic_object_exprt::set_instance(), string_constantt::set_value(), simplify_exprt::simplify_abs(), simplify_exprt::simplify_address_of(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_bswap(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_div(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_index(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_member(), simplify_exprt::simplify_minus(), simplify_exprt::simplify_mod(), simplify_exprt::simplify_mult(), simplify_exprt::simplify_object_size(), simplify_exprt::simplify_plus(), simplify_exprt::simplify_pointer_offset(), simplify_exprt::simplify_popcount(), simplify_exprt::simplify_power(), simplify_exprt::simplify_shifts(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_unary_minus(), size_of_expr(), unsignedbv_typet::smallest_expr(), signedbv_typet::smallest_expr(), stack_depth(), cpp_typecheckt::standard_conversion_array_to_pointer(), static_lifetime_init(), float_bvt::sticky_right_shift(), string_of_int_builtin_functiont::string_of_int_builtin_functiont(), float_bvt::sub_bias(), substitute_array_lists(), sum_over_map(), sum_overflows(), goto_symext::symex_allocate(), goto_symext::symex_cpp_new(), goto_symext::symex_other(), string_constantt::to_array_expr(), polynomialt::to_expr(), value_set_fit::to_expr(), value_set_fivrt::to_expr(), value_set_fivrnst::to_expr(), value_sett::to_expr(), sparse_arrayt::to_if_expression(), interval_sparse_arrayt::to_if_expression(), float_bvt::to_integer(), c_typecheck_baset::typecheck_c_enum_type(), c_typecheck_baset::typecheck_compound_body(), cpp_typecheckt::typecheck_enum_body(), c_typecheck_baset::typecheck_expr_alignof(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), c_typecheck_baset::typecheck_expr_dereference(), c_typecheck_baset::typecheck_expr_ptrmember(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_type(), c_typecheck_baset::typecheck_vector_type(), goto_checkt::undefined_shift_check(), float_bvt::unpack(), unpack_rec(), utf16_to_array(), string_abstractiont::value_assignments(), unsignedbv_typet::zero_expr(), signedbv_typet::zero_expr(), zero_if_negative(), and cpp_typecheckt::zero_initializer().
void mp_max | ( | mp_integer & | a, |
const mp_integer & | b | ||
) |
Definition at line 285 of file arith_tools.cpp.
void mp_min | ( | mp_integer & | a, |
const mp_integer & | b | ||
) |
Definition at line 279 of file arith_tools.cpp.
mp_integer power | ( | const mp_integer & | base, |
const mp_integer & | exponent | ||
) |
A multi-precision implementation of the power operator.
Definition at line 228 of file arith_tools.cpp.
References power(), and PRECONDITION.
Referenced by invariant_sett::add_type_bounds(), address_bits(), bv_arithmetict::adjust(), ieee_floatt::align(), ieee_float_spect::bias(), goto_checkt::conversion_check(), smt2_convt::convert_byte_update(), smt2_convt::convert_expr(), smt2_convt::convert_with(), ieee_floatt::extract_base10(), flatten_byte_update(), fixedbvt::format(), ieee_floatt::from_base10(), fixedbvt::from_integer(), generate_ansi_c_start_function(), float_utilst::get(), ieee_floatt::is_normal(), unsignedbv_typet::largest(), signedbv_typet::largest(), lower_popcount(), ieee_floatt::make_fltmax(), ieee_floatt::make_fltmin(), ieee_float_spect::max_exponent(), ieee_float_spect::max_fraction(), bv_spect::max_value(), bv_spect::min_value(), ieee_floatt::operator+=(), fixedbvt::operator/=(), ieee_floatt::operator/=(), operator<<(), fixedbvt::operator==(), operator>>(), overflow_instrumentert::overflow_expr(), bv_arithmetict::pack(), ieee_floatt::pack(), smt2_convt::parse_rec(), power(), fixedbvt::round(), simplify_exprt::simplify_bswap(), simplify_exprt::simplify_pointer_offset(), simplify_exprt::simplify_power(), simplify_exprt::simplify_shifts(), simplify_exprt::simplify_typecast(), signedbv_typet::smallest(), fixedbvt::to_integer(), ieee_floatt::to_integer(), ieee_floatt::to_string_decimal(), ieee_floatt::to_string_scientific(), and ieee_floatt::unpack().
bool to_integer | ( | const exprt & | expr, |
mp_integer & | int_value | ||
) |
Definition at line 17 of file arith_tools.cpp.
References exprt::is_constant(), to_constant_expr(), and to_integer().
Referenced by add_padding_gcc(), alignment(), interval_domaint::assume_rec(), simplify_exprt::bits2expr(), goto_checkt::bounds_check(), value_set_dereferencet::bounds_check(), string_abstractiont::build_array(), endianness_mapt::build_big_endian(), build_goto_trace(), build_sizeof_expr(), build_ssa_identifier_rec(), inv_object_storet::build_string(), boolbvt::bv_get_unbounded_array(), bv_refinementt::check_SAT(), compute_pointer_offset(), expr2ct::convert_array(), boolbvt::convert_array_of(), boolbvt::convert_byte_update(), smt2_convt::convert_byte_update(), java_bytecode_convert_methodt::convert_const(), expr2javat::convert_constant(), smt2_convt::convert_expr(), boolbvt::convert_extractbit(), boolbvt::convert_extractbits(), boolbvt::convert_index(), smt2_convt::convert_index(), java_bytecode_convert_methodt::convert_instructions(), boolbvt::convert_lambda(), smt2_convt::convert_minus(), smt2_convt::convert_plus(), expr2ct::convert_rec(), boolbvt::convert_replication(), boolbvt::convert_shift(), java_bytecode_convert_methodt::convert_switch(), smt2_convt::convert_typecast(), boolbvt::convert_update_rec(), bv_cbmct::convert_waitfor(), boolbvt::convert_with_array(), boolbvt::convert_with_bv(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), cpp_typecheckt::default_assignop_value(), smt2_convt::define_object_size(), c_typecheck_baset::designator_enter(), cpp_typecheck_resolvet::do_builtin(), c_typecheck_baset::do_initializer_rec(), bv_pointerst::do_postponed(), goto_convertt::do_prob_coin(), goto_convertt::do_prob_uniform(), c_typecheck_baset::do_special_functions(), interpretert::evaluate(), expr_initializert< nondet >::expr_initializer_rec(), smt2_convt::find_symbols_rec(), smt2_convt::flatten2bv(), smt2_convt::flatten_array(), flatten_byte_extract(), string_constantt::from_array_expr(), c_typecheck_baset::gcc_vector_types_compatible(), invariant_sett::get_bounds(), invariant_sett::get_constant(), boolbv_widtht::get_entry(), rw_range_sett::get_objects_byte_extract(), rw_range_sett::get_objects_index(), rw_range_sett::get_objects_shift(), get_quantifier_var_max(), value_set_fivrnst::get_reference_set_rec(), value_sett::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), interpretert::get_size(), get_subexpression_at_offset(), interpretert::get_value(), value_set_fit::get_value_set_rec(), value_set_fivrnst::get_value_set_rec(), value_set_fivrt::get_value_set_rec(), value_sett::get_value_set_rec(), simplify_exprt::get_values(), instantiate_quantifier(), is_dereference_integer_object(), boolbvt::is_unbounded_array(), boolbvt::literal(), c_typecheck_baset::make_designator(), format_constantt::operator()(), numeric_castt< mp_integer >::operator()(), smt2_convt::parse_rec(), pointer_offset_bits(), dereferencet::read_object(), remove_vector(), require_expr::require_index(), simplify_exprt::simplify_abs(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_bswap(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_div(), simplify_exprt::simplify_extractbit(), qdimacs_coret::simplify_extractbits(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_index(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_mod(), simplify_exprt::simplify_popcount(), simplify_exprt::simplify_power(), simplify_exprt::simplify_shifts(), simplify_exprt::simplify_sign(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_unary_minus(), simplify_exprt::simplify_update(), simplify_exprt::simplify_with(), invariant_sett::strengthen_rec(), goto_symext::symex_allocate(), goto_symext::symex_trace(), cpp_typecheckt::template_suffix(), to_integer(), string_constraint_generatort::to_integer_or_default(), to_unsigned_integer(), trace_numeric_value(), remove_const_function_pointerst::try_resolve_index_value(), type2name(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_c_bit_field_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_custom_type(), cpp_typecheckt::typecheck_enum_body(), c_typecheck_baset::typecheck_vector_type(), smt2_convt::unflatten(), unpack_rec(), unsigned_from_ns(), string_abstractiont::value_assignments(), java_bytecode_convert_methodt::variable(), xml(), and cpp_typecheckt::zero_initializer().
bool to_integer | ( | const constant_exprt & | expr, |
mp_integer & | int_value | ||
) |
Definition at line 24 of file arith_tools.cpp.
References binary2integer(), constant_exprt::get_value(), irept::id(), id2string(), string2integer(), typet::subtype(), to_c_enum_type(), and exprt::type().
bool to_unsigned_integer | ( | const constant_exprt & | expr, |
unsigned & | uint_value | ||
) |
convert a positive integer expression to an unsigned int
Definition at line 94 of file arith_tools.cpp.
References integer2unsigned(), and to_integer().
Referenced by string_constraint_generatort::add_axioms_for_format(), java_bytecode_convert_methodt::convert_instructions(), is_store_to_slot(), and utf16_constant_array_to_java().