java_string_literals.cpp File Reference

#include "java_string_literals.h"
#include "java_root_class.h"
#include "java_types.h"
#include "java_utils.h"
#include <util/arith_tools.h>
#include <util/expr_initializer.h>
#include <util/namespace.h>
#include <util/unicode.h>
#include <iomanip>
#include <sstream>

Include dependency graph for java_string_literals.cpp:

Go to the source code of this file.

Functions
static std::string	escape_non_alnum (const std::string &to_escape)
	Replace non-alphanumeric characters with _xx escapes, where xx are hex digits. More...
static array_exprt	utf16_to_array (const std::wstring &in)
	Convert UCS-2 or UTF-16 to an array expression. More...
symbol_exprt	get_or_create_string_literal_symbol (const exprt &string_expr, symbol_table_baset &symbol_table, bool string_refinement_enabled)
	Creates or gets an existing constant global symbol for a given string literal. More...

Function Documentation

escape_non_alnum()

static std::string escape_non_alnum ( const std::string &  to_escape )

static

Replace non-alphanumeric characters with _xx escapes, where xx are hex digits.

Underscores are replaced by __.

Parameters

to_escape

string to escape

Returns

string with non-alphanumeric characters escaped

Definition at line 26 of file java_string_literals.cpp.

Referenced by get_or_create_string_literal_symbol().

get_or_create_string_literal_symbol()

symbol_exprt get_or_create_string_literal_symbol	(	const exprt &	string_expr,
		symbol_table_baset &	symbol_table,
		bool	string_refinement_enabled
	)

Creates or gets an existing constant global symbol for a given string literal.

Parameters

string_expr	string literal expression to convert
symbol_table	global symbol table. If not already present, constant global symbols will be added.
string_refinement_enabled	if true, string refinement's string data structure will also be initialised and added to the symbol table.

Returns

a symbol_expr corresponding to the new or existing literal symbol.

Definition at line 66 of file java_string_literals.cpp.

References symbol_table_baset::add(), symbolt::base_name, exprt::copy_to_operands(), escape_non_alnum(), namespace_baset::follow(), from_integer(), irept::get(), irept::id(), id2string(), INVARIANT, symbolt::is_lvalue, symbolt::is_state_var, symbolt::is_static_lifetime, symbolt::is_type, java_int_type(), java_root_class_init(), JAVA_STRING_LITERAL_PREFIX, make_function_application(), symbolt::mode, exprt::move_to_operands(), symbolt::name, exprt::operands(), PRECONDITION, symbolt::pretty_name, irept::set(), data::size, exprt::source_location(), symbolt::symbol_expr(), symbol_table_baset::symbols, to_struct_type(), symbolt::type, exprt::type(), utf16_to_array(), utf8_to_utf16_native_endian(), symbolt::value, and zero_initializer().

Referenced by get_ldc_result(), and java_static_lifetime_init().

utf16_to_array()

static array_exprt utf16_to_array ( const std::wstring &  in )

static

Convert UCS-2 or UTF-16 to an array expression.

parameters: in: wide string to convert

Returns

Returns a Java char array containing the same wchars.

Definition at line 48 of file java_string_literals.cpp.

References exprt::copy_to_operands(), from_integer(), java_char_type(), and java_int_type().

Referenced by get_or_create_string_literal_symbol().