cprover
Deprecated primitives:
Member code_typet::code_typet ()
Member DEPRECATED ("use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead") void instrument_cover_goals(const symbol_tablet &symbol_table
use instrument_cover_goals(goto_programt &goto_program, const cover_instrumenterst &instrumenters, message_handlert &message_handler, const irep_idt mode) instead
Member integer2size_t (const mp_integer &)
use numeric_cast_v<std::size_t> instead
Member integer2size_t (const mp_integer &)
use numeric_cast_v<std::size_t> instead
Member integer2ulong (const mp_integer &)
use numeric_cast_v<unsigned long long> instead
Member integer2ulong (const mp_integer &)
use numeric_cast_v<unsigned long long> instead
Member integer2unsigned (const mp_integer &)
use numeric_cast_v<unsigned> instead
Member integer2unsigned (const mp_integer &)
use numeric_cast_v<unsigned> instead
Member string_constraint_generatort::add_axioms_for_code_point_count (const function_application_exprt &f)
This is Java specific and should be implemented in Java.
Member string_constraint_generatort::add_axioms_for_concat (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
should use concat_substr instead
Member string_constraint_generatort::add_axioms_for_concat_code_point (const function_application_exprt &f)
java specific
Member string_constraint_generatort::add_axioms_for_copy (const function_application_exprt &f)
should use substring instead
Member string_constraint_generatort::add_axioms_for_insert_bool (const function_application_exprt &f)
should convert the value to string and call insert
Member string_constraint_generatort::add_axioms_for_insert_double (const function_application_exprt &f)
should convert the value to string and call insert
Member string_constraint_generatort::add_axioms_for_insert_float (const function_application_exprt &f)
should convert the value to string and call insert
Member string_constraint_generatort::add_axioms_for_insert_int (const function_application_exprt &f)
should convert the value to string and call insert
Member string_constraint_generatort::add_axioms_for_intern (const function_application_exprt &f)

Not tested.

never tested

Member string_constraint_generatort::add_axioms_for_is_empty (const function_application_exprt &f)
should use string_length(s)==0 instead
Member string_constraint_generatort::add_axioms_for_offset_by_code_point (const function_application_exprt &f)
This is Java specific and should be implemented in Java.
Member string_constraint_generatort::add_axioms_from_bool (const function_application_exprt &f)
This is Java specific and should be implemented in Java instead
Member string_constraint_generatort::add_axioms_from_bool (const array_string_exprt &res, const exprt &i)
This is Java specific and should be implemented in Java instead
Member string_constraint_generatort::add_axioms_from_int_hex (const array_string_exprt &res, const exprt &i)
use add_axioms_from_int which takes a radix argument instead
Member string_constraint_generatort::add_axioms_from_long (const function_application_exprt &f)
should use add_axioms_from_int instead
Member to_integer (const exprt &expr, mp_integer &int_value)
: use the constant_exprt version instead