cprover
|
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_preprocesst | private |
blue | messaget | static |
bold | messaget | static |
bright_blue | messaget | static |
bright_cyan | messaget | static |
bright_green | messaget | static |
bright_magenta | messaget | static |
bright_red | messaget | static |
bright_yellow | messaget | static |
char_type | java_string_library_preprocesst | private |
character_preprocess | java_string_library_preprocesst | private |
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_preprocesst | private |
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_preprocesst | private |
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_preprocesst | private |
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_preprocesst | private |
command(unsigned c) | messaget | inlinestatic |
conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const | messaget | |
conversion_functiont typedef | java_string_library_preprocesst | private |
conversion_table | java_string_library_preprocesst | private |
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_preprocesst | private |
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_preprocesst | friend |
cprover_equivalent_to_java_assign_and_return_function | java_string_library_preprocesst | private |
cprover_equivalent_to_java_assign_function | java_string_library_preprocesst | private |
cprover_equivalent_to_java_constructor | java_string_library_preprocesst | private |
cprover_equivalent_to_java_function | java_string_library_preprocesst | private |
cprover_equivalent_to_java_string_returning_function | java_string_library_preprocesst | private |
cyan | messaget | static |
debug() const | messaget | inline |
decl_string_expr(const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code) | java_string_library_preprocesst | private |
eom | messaget | static |
error() const | messaget | inline |
eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest) | messaget | static |
faint | messaget | static |
fresh_string(const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) | java_string_library_preprocesst | private |
get_all_function_names(std::unordered_set< irep_idt > &methods) const | java_string_library_preprocesst | |
get_message_handler() | messaget | inline |
get_mstream(unsigned message_level) const | messaget | inline |
get_string_type_base_classes(const irep_idt &class_name) | java_string_library_preprocesst | |
green | messaget | static |
id_maps | java_string_library_preprocesst | private |
id_mapt typedef | java_string_library_preprocesst | private |
implements_function(const irep_idt &function_id) const | java_string_library_preprocesst | |
implements_java_char_sequence(const typet &type) | java_string_library_preprocesst | inlinestatic |
implements_java_char_sequence_pointer(const typet &type) | java_string_library_preprocesst | inlinestatic |
index_type | java_string_library_preprocesst | private |
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_preprocesst | privatestatic |
is_java_char_array_type(const typet &type) | java_string_library_preprocesst | privatestatic |
is_java_char_sequence_pointer_type(const typet &type) | java_string_library_preprocesst | privatestatic |
is_java_char_sequence_type(const typet &type) | java_string_library_preprocesst | privatestatic |
is_java_string_buffer_pointer_type(const typet &type) | java_string_library_preprocesst | privatestatic |
is_java_string_buffer_type(const typet &type) | java_string_library_preprocesst | privatestatic |
is_java_string_builder_pointer_type(const typet &type) | java_string_library_preprocesst | privatestatic |
is_java_string_builder_type(const typet &type) | java_string_library_preprocesst | privatestatic |
is_java_string_pointer_type(const typet &type) | java_string_library_preprocesst | privatestatic |
is_java_string_type(const typet &type) | java_string_library_preprocesst | privatestatic |
is_known_string_type(irep_idt class_name) | java_string_library_preprocesst | |
italic | messaget | static |
java_string_library_preprocesst() | java_string_library_preprocesst | inline |
java_string_library_preprocesst(const java_string_library_preprocesst &)=delete | java_string_library_preprocesst | private |
java_type_matches_tag(const typet &type, const std::string &tag) | java_string_library_preprocesst | privatestatic |
M_DEBUG enum value | messaget | |
M_ERROR enum value | messaget | |
M_PROGRESS enum value | messaget | |
M_RESULT enum value | messaget | |
M_STATISTICS enum value | messaget | |
M_STATUS enum value | messaget | |
M_WARNING enum value | messaget | |
magenta | messaget | static |
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_preprocesst | private |
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_preprocesst | private |
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_preprocesst | private |
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_preprocesst | private |
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_preprocesst | private |
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_preprocesst | private |
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_preprocesst | private |
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_preprocesst | private |
make_nondet_string_expr(const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code) | java_string_library_preprocesst | private |
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_preprocesst | private |
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_preprocesst | private |
message_handler | messaget | protected |
message_levelt enum name | messaget | |
messaget() | messaget | inline |
messaget(const messaget &other) | messaget | inline |
messaget(message_handlert &_message_handler) | messaget | inlineexplicit |
mstream | messaget | mutableprotected |
operator=(const messaget &other) | messaget | inline |
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_preprocesst | private |
process_parameters(const java_method_typet::parameterst ¶ms, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &init_code) | java_string_library_preprocesst | private |
progress() const | messaget | inline |
red | messaget | static |
refined_string_type | java_string_library_preprocesst | private |
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_preprocesst | private |
replace_character_call(code_function_callt call) | java_string_library_preprocesst | inline |
reset | messaget | static |
result() const | messaget | inline |
set_message_handler(message_handlert &_message_handler) | messaget | inlinevirtual |
statistics() const | messaget | inline |
status() const | messaget | inline |
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_preprocesst | private |
string_literal_to_string_expr(const std::string &s, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code) | java_string_library_preprocesst | private |
string_types | java_string_library_preprocesst | private |
underline | messaget | static |
warning() const | messaget | inline |
yellow | messaget | static |
~messaget() | messaget | virtual |