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_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_name, 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, 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, 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, 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_array(const typet &type, const source_locationt &loc, symbol_tablet &symbol_table)	java_string_library_preprocesst	private
fresh_string(const typet &type, const source_locationt &loc, 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_object_at_index(const exprt &argv, std::size_t index)	java_string_library_preprocesst	private
get_primitive_value_of_object(const exprt &object, irep_idt type_name, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)	java_string_library_preprocesst	private
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_argument_for_format(const exprt &argv, std::size_t index, const struct_typet &structured_type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)	java_string_library_preprocesst	private
make_assign_and_return_function_from_call(const irep_idt &function_name, 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_name, const java_method_typet &type, const source_locationt &loc, 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_name, 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_name, 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_object_get_class_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_format_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_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_name, 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_equals_function_operands(const exprt::operandst &operands, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)	java_string_library_preprocesst	private
process_operands(const exprt::operandst &operands, const source_locationt &loc, 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, 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, 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_name, 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