- 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_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 array_string_exprt &res, const exprt &b)
- This is Java specific and should be implemented in Java instead
- 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_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 goto_program_dereferencet::dereference_failure (const std::string &property, const std::string &msg, const guardt &guard)
- Member goto_program_dereferencet::is_valid_object (const irep_idt &identifier)
- Member instrument_cover_goals (const symbol_tablet &, goto_programt &, coverage_criteriont, 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 instrument_cover_goals (const symbol_tablet &, goto_programt &, coverage_criteriont, 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
- Member irept::get_unsigned_int (const irep_namet &name) const
- use get_size_t instead
- Class nil_typet
- Use
optional<typet>
instead.
- Member pointer_checks (goto_functionst &, symbol_tablet &, const optionst &, value_setst &)
- Member pointer_checks (goto_programt &, symbol_tablet &, const optionst &, value_setst &)
- Member pointer_checks (goto_programt &, symbol_tablet &, const optionst &, value_setst &)
- Member pointer_checks (goto_functionst &, symbol_tablet &, const optionst &, value_setst &)
- Member read_goto_binary (const std::string &filename, goto_modelt &dest, message_handlert &)
- Use read_goto_binary(file, message_handler) instead
- Member read_goto_binary (const std::string &filename, goto_modelt &dest, message_handlert &)
- Use read_goto_binary(file, message_handler) instead
- Member remove_pointers (goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets)
- Member string_constraint_generatort::add_axioms_for_intern (symbol_generatort &fresh_symbol, const function_application_exprt &f)
Not tested.
never tested
- Member to_integer (const exprt &expr, mp_integer &int_value)
- : use the constant_exprt version instead