cprover
Deprecated List
Member add_axioms_for_code_point_count (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
This is Java specific and should be implemented in Java.
Member add_axioms_for_code_point_count (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
This is Java specific and should be implemented in Java.
Member add_axioms_for_concat (symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
should use concat_substr instead
Member add_axioms_for_concat_code_point (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
java specific
Member add_axioms_for_copy (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
should use substring instead
Member add_axioms_for_insert_bool (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
should convert the value to string and call insert
Member add_axioms_for_insert_double (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
should convert the value to string and call insert
Member add_axioms_for_insert_float (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
should convert the value to string and call insert
Member add_axioms_for_insert_int (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
should convert the value to string and call insert
Member add_axioms_for_is_empty (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
should use string_length(s)==0 instead
Member add_axioms_for_is_suffix (symbol_generatort &fresh_symbol, const function_application_exprt &f, bool swap_arguments, array_poolt &array_pool)
Should use strings_startwith(s0, s1, s1.length - s0.length).
Member add_axioms_for_offset_by_code_point (symbol_generatort &fresh_symbol, const function_application_exprt &f)
This is Java specific and should be implemented in Java.
Member add_axioms_from_bool (const function_application_exprt &f, array_poolt &array_pool)
This is Java specific and should be implemented in Java instead
Member add_axioms_from_bool (const array_string_exprt &res, const exprt &b)
This is Java specific and should be implemented in Java instead
Member add_axioms_from_bool (const array_string_exprt &res, const exprt &b)
This is Java specific and should be implemented in Java instead
Member add_axioms_from_int_hex (const array_string_exprt &res, const exprt &i)
use add_axioms_from_int_with_radix instead
Member add_axioms_from_long (const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
should use add_axioms_from_int instead
Class class_hierarchyt
class_hierarchy_grapht is a more advanced graph-based representation of the class hierarchy and its use is preferred over class_hierarchy_classt.
Member code_typet::code_typet ()
Member exprt::make_bool (bool value)
use constructors instead
Member exprt::make_typecast (const typet &_type)
use constructors instead
Member instrument_cover_goals (const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, coverage_criteriont criterion, message_handlert &message_handler)
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
Class nil_typet
Use optional<typet> instead.
Member string_constraint_generatort::add_axioms_for_intern (const function_application_exprt &f)

Not tested.

never tested