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)
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.
type.
set(ID_C_constant,
true);
88 new_symbol.
base_name = escaped_symbol_name;
90 new_symbol.
mode = ID_java;
107 if(string_refinement_enabled)
113 literal_init.
operands().resize(jls_struct.components().size());
114 const std::size_t jlo_nb = jls_struct.component_number(
"@java.lang.Object");
115 literal_init.
operands()[jlo_nb] = jlo_init;
117 const std::size_t length_nb = jls_struct.component_number(
"length");
118 const typet &length_type = jls_struct.components()[length_nb].type();
120 literal_init.
operands()[length_nb] = length;
124 array_symbol.
name = escaped_symbol_name_with_prefix +
"_constarray";
125 array_symbol.
base_name = escaped_symbol_name +
"_constarray";
127 array_symbol.
mode = ID_java;
135 array_symbol.
type.
set(ID_C_constant,
true);
137 if(symbol_table.
add(array_symbol))
138 throw "failed to add constarray symbol to symbol table";
144 const std::size_t data_nb = jls_struct.component_number(
"data");
145 literal_init.
operands()[data_nb] = array_pointer;
149 return_symbol.
name = escaped_symbol_name_with_prefix +
"_return_value";
150 return_symbol.
base_name = escaped_symbol_name +
"_return_value";
152 escaped_symbol_name.length() > 10
153 ? escaped_symbol_name.substr(0, 10) +
"..._return_value" 154 : escaped_symbol_name +
"_return_value";
155 return_symbol.
mode = ID_java;
161 ID_cprover_associate_array_to_pointer_func,
162 {array_symbol.
value, array_pointer},
166 return_symbol.
type.
set(ID_C_constant,
true);
167 if(symbol_table.
add(return_symbol))
168 throw "failed to add return symbol to symbol table";
174 exprt init_comma_expr(ID_comma);
175 init_comma_expr.
type() = literal_init.
type();
178 new_symbol.
value = init_comma_expr;
180 else if(jls_struct.components().size()>=1 &&
181 jls_struct.components()[0].get_name()==
"@java.lang.Object")
188 for(
const auto &comp : jls_struct.components())
190 if(comp.get_name()==
"@java.lang.Object")
200 new_symbol.
value = literal_init;
206 new_symbol.
value = jlo_init;
209 bool add_failed = symbol_table.
add(new_symbol);
212 "string literal symbol was already checked not to be " 213 "in the symbol table, so adding it should succeed");
The type of an expression, extends irept.
irep_idt name
The unique identifier.
#define JAVA_STRING_LITERAL_PREFIX
const std::string & id2string(const irep_idt &d)
std::wstring utf8_to_utf16_native_endian(const std::string &in)
Convert UTF8-encoded string to UTF-16 with architecture-native endianness.
irep_idt mode
Language mode.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
exprt value
Initial value of symbol.
A struct tag type, i.e., struct_typet with an identifier.
irep_idt pretty_name
Language-specific display name.
typet & type()
Return the type of the expression.
#define CHECK_RETURN(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Expression Initialization.
const irep_idt & id() const
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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.
typet type
Type of symbol.
Base class for all expressions.
void java_root_class_init(struct_exprt &jlo, const struct_typet &root_type, const irep_idt &class_identifier)
Adds members for an object of the root class (usually java.lang.Object).
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.
const java_class_typet & to_java_class_type(const typet &type)
void set(const irep_namet &name, const irep_idt &value)