CBMC: Member List

add_string_type(const irep_idt &class_name, symbol_table_baset &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

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, message_handlert &message_handler) 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

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 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

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

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_string_type_base_classes(const irep_idt &class_name) java_string_library_preprocesst

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

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

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, message_handlert &message_handler) 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, message_handlert &message_handler) 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, message_handlert &message_handler) 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, message_handlert &message_handler) 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, message_handlert &message_handler) 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

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 &params, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &init_code) java_string_library_preprocesst private

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

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