cprover
arith_tools.h File Reference
#include "invariant.h"
#include "mp_arith.h"
#include "optional.h"
#include "std_expr.h"
#include "deprecate.h"
Include dependency graph for arith_tools.h:

Go to the source code of this file.

Classes

struct  numeric_castt< Target, typename >
 Numerical cast provides a unified way of converting from one numerical type to another. More...
 
struct  numeric_castt< mp_integer >
 Convert expression to mp_integer. More...
 
struct  numeric_castt< T, typename std::enable_if< std::is_integral< T >::value >::type >
 Convert mp_integer or expr to any integral type. More...
 

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...
 
template<typename Target >
optionalt< Target > numeric_cast (const exprt &arg)
 Converts an expression to any integral type. More...
 
template<typename Target >
Target numeric_cast_v (const mp_integer &arg)
 Convert an mp_integer to integral type Target An invariant with fail with message "Bad conversion" if conversion is not possible. More...
 
template<typename Target >
Target numeric_cast_v (const exprt &arg)
 Convert an expression to integral type Target An invariant with fail with message "Bad conversion" if conversion is not possible. 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)
 

Function Documentation

◆ address_bits()

◆ from_integer()

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().

◆ mp_max()

void mp_max ( mp_integer a,
const mp_integer b 
)

Definition at line 285 of file arith_tools.cpp.

◆ mp_min()

void mp_min ( mp_integer a,
const mp_integer b 
)

Definition at line 279 of file arith_tools.cpp.

◆ numeric_cast()

template<typename Target >
optionalt<Target> numeric_cast ( const exprt arg)

Converts an expression to any integral type.

Template Parameters
Targettype to convert to
Parameters
argexpression to convert
Returns
optional integer of type Target if conversion is possible, empty optional otherwise.

Definition at line 122 of file arith_tools.h.

Referenced by add_to_index_set(), boolbvt::convert_byte_extract(), goto_convertt::convert_gcc_switch_case_range(), string_set_char_builtin_functiont::eval(), string_of_int_builtin_functiont::eval(), get_array(), havoc_generate_function_bodiest::havoc_expr_rec(), interval_sparse_arrayt::interval_sparse_arrayt(), string_of_int_builtin_functiont::length_constraint(), substitute_array_lists(), and to_char_pair().

◆ numeric_cast_v() [1/2]

template<typename Target >
Target numeric_cast_v ( const mp_integer arg)

Convert an mp_integer to integral type Target An invariant with fail with message "Bad conversion" if conversion is not possible.

Template Parameters
Targettype to convert to
Parameters
argmp_integer
Returns
value of type Target

Definition at line 134 of file arith_tools.h.

References INVARIANT.

◆ numeric_cast_v() [2/2]

template<typename Target >
Target numeric_cast_v ( const exprt arg)

Convert an expression to integral type Target An invariant with fail with message "Bad conversion" if conversion is not possible.

Template Parameters
Targettype to convert to
Parameters
argconstant expression
Returns
value of type Target

Definition at line 148 of file arith_tools.h.

References INVARIANT.

◆ power()

mp_integer power ( const mp_integer base,
const mp_integer exponent 
)

A multi-precision implementation of the power operator.

parameters: Two mp_integers, base and exponent
Returns
One mp_integer with the value base^{exponent}

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().

◆ to_integer() [1/2]

bool to_integer ( const exprt expr,
mp_integer int_value 
)
Deprecated:
: use the constant_exprt version instead

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().

◆ to_integer() [2/2]

bool to_integer ( const constant_exprt expr,
mp_integer int_value 
)

◆ to_unsigned_integer()

bool to_unsigned_integer ( const constant_exprt expr,
unsigned &  uint_value 
)

convert a positive integer expression to an unsigned int

parameters: a constant expression and a reference to an unsigned int
Returns
an error flag

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().