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_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_false ()
use constructors instead
Member exprt::make_not ()
use constructors instead
Member exprt::make_true ()
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_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 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