31 for(
const auto c : in)
39 bool string_refinement_enabled)
50 return findit->second.symbol_expr();
52#ifndef CPROVER_INVARIANT_DO_NOT_CHECK
63 new_symbol.pretty_name = value;
64 new_symbol.is_lvalue =
true;
65 new_symbol.is_state_var =
true;
66 new_symbol.is_static_lifetime =
true;
80 if(string_refinement_enabled)
99 array_symbol.pretty_name = value;
100 array_symbol.is_lvalue =
true;
102 array_symbol.is_static_lifetime =
true;
103 array_symbol.is_state_var =
true;
104 array_symbol.value = data;
107 if(symbol_table.
add(array_symbol))
108 throw "failed to add constarray symbol to symbol table";
136 throw "failed to add return symbol to symbol table";
149 jls_struct.components()[0].get_name()==
"@java.lang.Object")
157 if(
comp.get_name()==
"@java.lang.Object")
180 "string literal symbol was already checked not to be "
181 "in the symbol table, so adding it should succeed");
183 return new_symbol.symbol_expr();
189 bool string_refinement_enabled)
194 string_refinement_enabled);
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Array constructor from list of elements.
const array_typet & type() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Struct constructor from list of elements.
A struct tag type, i.e., struct_typet with an identifier.
Expression to hold a symbol (variable)
The symbol table base class interface.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
The type of an expression, extends irept.
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
const std::string & id2string(const irep_idt &d)
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).
Representation of a constant Java string.
static array_exprt utf16_to_array(const std::wstring &in)
Convert UCS-2 or UTF-16 to an array expression.
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.
signedbv_typet java_int_type()
unsignedbv_typet java_char_type()
const java_class_typet & to_java_class_type(const typet &type)
exprt make_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &range, symbol_table_baset &symbol_table)
Create a (mathematical) function application expression.
#define JAVA_STRING_LITERAL_PREFIX
#define CHECK_RETURN(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define INITIALIZE_FUNCTION
std::string escape_non_alnum(const std::string &to_escape)
Replace non-alphanumeric characters with _xx escapes, where xx are hex digits.
std::wstring utf8_to_utf16_native_endian(const std::string &in)
Convert UTF8-encoded string to UTF-16 with architecture-native endianness.