cprover
java_string_literals.h File Reference
#include <util/symbol_table.h>
#include <util/std_expr.h>
Include dependency graph for java_string_literals.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

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

◆ 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_exprstring literal expression to convert
symbol_tableglobal symbol table. If not already present, constant global symbols will be added.
string_refinement_enabledif 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, 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_little_endian(), symbolt::value, and zero_initializer().

Referenced by get_ldc_result(), and java_static_lifetime_init().