cprover
java_string_library_preprocesst Member List

This is the complete list of members for java_string_library_preprocesst, including all inherited members.

add_string_type(const irep_idt &class_name, symbol_tablet &symbol_table)java_string_library_preprocesst
allocate_fresh_string(const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)java_string_library_preprocesstprivate
bluemessagetstatic
boldmessagetstatic
bright_bluemessagetstatic
bright_cyanmessagetstatic
bright_greenmessagetstatic
bright_magentamessagetstatic
bright_redmessagetstatic
bright_yellowmessagetstatic
char_typejava_string_library_preprocesstprivate
character_preprocessjava_string_library_preprocesstprivate
code_assign_components_to_java_string(const exprt &lhs, const exprt &rhs_array, const exprt &rhs_length, const symbol_table_baset &symbol_table, bool is_constructor)java_string_library_preprocesstprivate
code_assign_java_string_to_string_expr(const refined_string_exprt &lhs, const exprt &rhs, const source_locationt &loc, const symbol_table_baset &symbol_table, code_blockt &code)java_string_library_preprocesstprivate
code_assign_string_expr_to_java_string(const exprt &lhs, const refined_string_exprt &rhs, const symbol_table_baset &symbol_table, bool is_constructor)java_string_library_preprocesstprivate
code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table)java_string_library_preprocesst
code_return_function_application(const irep_idt &function_id, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)java_string_library_preprocesstprivate
command(unsigned c)messagetinlinestatic
conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) constmessaget
conversion_functiont typedefjava_string_library_preprocesstprivate
conversion_tablejava_string_library_preprocesstprivate
convert_exprt_to_string_exprt(const exprt &deref, const source_locationt &loc, symbol_table_baset &symbol_table, const irep_idt &function_name, code_blockt &init_code)java_string_library_preprocesstprivate
convert_exprt_to_string_exprt_unit_test(java_string_library_preprocesst &preprocess, const exprt &deref, const source_locationt &loc, const irep_idt &function_id, symbol_tablet &symbol_table, code_blockt &init_code)java_string_library_preprocesstfriend
cprover_equivalent_to_java_assign_and_return_functionjava_string_library_preprocesstprivate
cprover_equivalent_to_java_assign_functionjava_string_library_preprocesstprivate
cprover_equivalent_to_java_constructorjava_string_library_preprocesstprivate
cprover_equivalent_to_java_functionjava_string_library_preprocesstprivate
cprover_equivalent_to_java_string_returning_functionjava_string_library_preprocesstprivate
cyanmessagetstatic
debug() constmessagetinline
decl_string_expr(const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)java_string_library_preprocesstprivate
eommessagetstatic
error() constmessagetinline
eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)messagetstatic
faintmessagetstatic
fresh_string(const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)java_string_library_preprocesstprivate
get_all_function_names(std::unordered_set< irep_idt > &methods) constjava_string_library_preprocesst
get_message_handler()messagetinline
get_mstream(unsigned message_level) constmessagetinline
get_string_type_base_classes(const irep_idt &class_name)java_string_library_preprocesst
greenmessagetstatic
id_mapsjava_string_library_preprocesstprivate
id_mapt typedefjava_string_library_preprocesstprivate
implements_function(const irep_idt &function_id) constjava_string_library_preprocesst
implements_java_char_sequence(const typet &type)java_string_library_preprocesstinlinestatic
implements_java_char_sequence_pointer(const typet &type)java_string_library_preprocesstinlinestatic
index_typejava_string_library_preprocesstprivate
initialize_conversion_table()java_string_library_preprocesst
initialize_known_type_table()java_string_library_preprocesst
is_java_char_array_pointer_type(const typet &type)java_string_library_preprocesstprivatestatic
is_java_char_array_type(const typet &type)java_string_library_preprocesstprivatestatic
is_java_char_sequence_pointer_type(const typet &type)java_string_library_preprocesstprivatestatic
is_java_char_sequence_type(const typet &type)java_string_library_preprocesstprivatestatic
is_java_string_buffer_pointer_type(const typet &type)java_string_library_preprocesstprivatestatic
is_java_string_buffer_type(const typet &type)java_string_library_preprocesstprivatestatic
is_java_string_builder_pointer_type(const typet &type)java_string_library_preprocesstprivatestatic
is_java_string_builder_type(const typet &type)java_string_library_preprocesstprivatestatic
is_java_string_pointer_type(const typet &type)java_string_library_preprocesstprivatestatic
is_java_string_type(const typet &type)java_string_library_preprocesstprivatestatic
is_known_string_type(irep_idt class_name)java_string_library_preprocesst
italicmessagetstatic
java_string_library_preprocesst()java_string_library_preprocesstinline
java_string_library_preprocesst(const java_string_library_preprocesst &)=deletejava_string_library_preprocesstprivate
java_type_matches_tag(const typet &type, const std::string &tag)java_string_library_preprocesstprivatestatic
M_DEBUG enum valuemessaget
M_ERROR enum valuemessaget
M_PROGRESS enum valuemessaget
M_RESULT enum valuemessaget
M_STATISTICS enum valuemessaget
M_STATUS enum valuemessaget
M_WARNING enum valuemessaget
magentamessagetstatic
make_assign_and_return_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)java_string_library_preprocesstprivate
make_assign_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)java_string_library_preprocesstprivate
make_class_identifier_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)java_string_library_preprocesstprivate
make_copy_constructor_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)java_string_library_preprocesstprivate
make_copy_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)java_string_library_preprocesstprivate
make_float_to_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)java_string_library_preprocesstprivate
make_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)java_string_library_preprocesstprivate
make_init_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool is_constructor=true)java_string_library_preprocesstprivate
make_nondet_string_expr(const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)java_string_library_preprocesstprivate
make_string_length_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)java_string_library_preprocesstprivate
make_string_returning_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)java_string_library_preprocesstprivate
message_handlermessagetprotected
message_levelt enum namemessaget
messaget()messagetinline
messaget(const messaget &other)messagetinline
messaget(message_handlert &_message_handler)messagetinlineexplicit
mstreammessagetmutableprotected
operator=(const messaget &other)messagetinline
process_operands(const exprt::operandst &operands, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &init_code)java_string_library_preprocesstprivate
process_parameters(const java_method_typet::parameterst &params, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &init_code)java_string_library_preprocesstprivate
progress() constmessagetinline
redmessagetstatic
refined_string_typejava_string_library_preprocesstprivate
replace_char_array(const exprt &array_pointer, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &code)java_string_library_preprocesstprivate
replace_character_call(code_function_callt call)java_string_library_preprocesstinline
resetmessagetstatic
result() constmessagetinline
set_message_handler(message_handlert &_message_handler)messagetinlinevirtual
statistics() constmessagetinline
status() constmessagetinline
string_expr_of_function(const irep_idt &function_id, const exprt::operandst &arguments, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)java_string_library_preprocesstprivate
string_literal_to_string_expr(const std::string &s, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)java_string_library_preprocesstprivate
string_typesjava_string_library_preprocesstprivate
underlinemessagetstatic
warning() constmessagetinline
yellowmessagetstatic
~messaget()messagetvirtual