28 std::ostringstream escaped;
29 for(
auto &ch : to_escape)
53 for(
const auto c : in)
67 const exprt &string_expr,
69 bool string_refinement_enabled)
73 const symbol_typet string_type(
"java::java.lang.String");
76 const std::string escaped_symbol_name_with_prefix =
79 auto findit = symbol_table.
symbols.find(escaped_symbol_name_with_prefix);
80 if(findit != symbol_table.
symbols.end())
81 return findit->second.symbol_expr();
85 new_symbol.
name = escaped_symbol_name_with_prefix;
86 new_symbol.
type = string_type;
87 new_symbol.
base_name = escaped_symbol_name;
89 new_symbol.
mode = ID_java;
106 if(string_refinement_enabled)
112 literal_init.
operands().resize(jls_struct.components().size());
113 const std::size_t jlo_nb = jls_struct.component_number(
"@java.lang.Object");
114 literal_init.
operands()[jlo_nb] = jlo_init;
116 const std::size_t length_nb = jls_struct.component_number(
"length");
117 const typet &length_type = jls_struct.components()[length_nb].type();
119 literal_init.
operands()[length_nb] = length;
123 array_symbol.
name = escaped_symbol_name_with_prefix +
"_constarray";
124 array_symbol.
base_name = escaped_symbol_name +
"_constarray";
126 array_symbol.
mode = ID_java;
135 if(symbol_table.
add(array_symbol))
136 throw "failed to add constarray symbol to symbol table";
142 const std::size_t data_nb = jls_struct.component_number(
"data");
143 literal_init.
operands()[data_nb] = array_pointer;
147 return_symbol.
name = escaped_symbol_name_with_prefix +
"_return_value";
148 return_symbol.
base_name = escaped_symbol_name +
"_return_value";
150 escaped_symbol_name.length() > 10
151 ? escaped_symbol_name.substr(0, 10) +
"..._return_value" 152 : escaped_symbol_name +
"_return_value";
153 return_symbol.
mode = ID_java;
159 ID_cprover_associate_array_to_pointer_func,
160 {array_symbol.
value, array_pointer},
164 if(symbol_table.
add(return_symbol))
165 throw "failed to add return symbol to symbol table";
171 exprt init_comma_expr(ID_comma);
172 init_comma_expr.
type() = literal_init.
type();
175 new_symbol.
value = init_comma_expr;
177 else if(jls_struct.components().size()>=1 &&
178 jls_struct.components()[0].get_name()==
"@java.lang.Object")
185 for(
const auto &comp : jls_struct.components())
187 if(comp.get_name()==
"@java.lang.Object")
195 new_symbol.
value = literal_init;
197 else if(jls_struct.get_bool(ID_incomplete_class))
201 new_symbol.
value = jlo_init;
204 bool add_failed = symbol_table.
add(new_symbol);
207 "string literal symbol was already checked not to be " 208 "in the symbol table, so adding it should succeed");
The type of an expression.
irep_idt name
The unique identifier.
#define JAVA_STRING_LITERAL_PREFIX
const std::string & id2string(const irep_idt &d)
irep_idt mode
Language mode.
void copy_to_operands(const exprt &expr)
void move_to_operands(exprt &expr)
exprt value
Initial value of symbol.
irep_idt pretty_name
Language-specific display name.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
#define INVARIANT(CONDITION, REASON)
Expression Initialization.
const irep_idt & id() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
A reference into the symbol table.
exprt make_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)
Create a function application expression.
const irep_idt & get(const irep_namet &name) const
#define PRECONDITION(CONDITION)
const typet & follow(const typet &) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Operator to return the address of an object.
static std::string escape_non_alnum(const std::string &to_escape)
Replace non-alphanumeric characters with _xx escapes, where xx are hex digits.
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
void java_root_class_init(struct_exprt &jlo, const struct_typet &root_type, const bool lock, const irep_idt &class_identifier)
Adds members for an object of the root class (usually java.lang.Object).
std::wstring utf8_to_utf16_little_endian(const std::string &in)
typet type
Type of symbol.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
The symbol table base class interface.
const source_locationt & source_location() const
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.
Expression to hold a symbol (variable)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
static array_exprt utf16_to_array(const std::wstring &in)
Convert UCS-2 or UTF-16 to an array expression.
struct constructor from list of elements
array constructor from list of elements