|
CBMC
|
#include "java_string_literals.h"#include "java_root_class.h"#include "java_string_literal_expr.h"#include "java_types.h"#include "java_utils.h"#include <linking/static_lifetime_init.h>#include <util/arith_tools.h>#include <util/expr_initializer.h>#include <util/namespace.h>#include <util/string_utils.h>#include <util/symbol_table_base.h>#include <util/unicode.h>#include <sstream>
Include dependency graph for java_string_literals.cpp:Go to the source code of this file.
Functions | |
| 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 java_string_literal_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... | |
| symbol_exprt | get_or_create_string_literal_symbol (const irep_idt &string_value, symbol_table_baset &symbol_table, bool string_refinement_enabled) |
| Same as get_or_create_string_literal_symbol(const exprt&, symbol_table_baset&, bool) except it takes an id/string parameter rather than a string literal exprt. More... | |
| symbol_exprt get_or_create_string_literal_symbol | ( | const irep_idt & | string_value, |
| symbol_table_baset & | symbol_table, | ||
| bool | string_refinement_enabled | ||
| ) |
Same as get_or_create_string_literal_symbol(const exprt&, symbol_table_baset&, bool) except it takes an id/string parameter rather than a string literal exprt.
Definition at line 197 of file java_string_literals.cpp.
| symbol_exprt get_or_create_string_literal_symbol | ( | const java_string_literal_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.
| 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. |
Definition at line 38 of file java_string_literals.cpp.
|
static |
Convert UCS-2 or UTF-16 to an array expression.
Definition at line 28 of file java_string_literals.cpp.