39 bool string_refinement_enabled)
45 const std::string escaped_symbol_name_with_prefix =
48 auto findit = symbol_table.
symbols.find(escaped_symbol_name_with_prefix);
49 if(findit != symbol_table.
symbols.end())
50 return findit->second.symbol_expr();
52#ifndef CPROVER_INVARIANT_DO_NOT_CHECK
55 !initialize_function || initialize_function->value.is_nil(),
60 symbolt new_symbol{escaped_symbol_name_with_prefix, string_type, ID_java};
61 new_symbol.type.
set(ID_C_constant,
true);
62 new_symbol.base_name = escaped_symbol_name;
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)
86 literal_init.
operands().resize(jls_struct.components().size());
87 const std::size_t jlo_nb = jls_struct.component_number(
"@java.lang.Object");
88 literal_init.operands()[jlo_nb] = jlo_init;
90 const std::size_t length_nb = jls_struct.component_number(
"length");
91 const typet &length_type = jls_struct.components()[length_nb].type();
93 literal_init.operands()[length_nb] = length;
97 escaped_symbol_name_with_prefix +
"_constarray",
data.type(), ID_java};
98 array_symbol.base_name = escaped_symbol_name +
"_constarray";
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;
105 array_symbol.type.set(ID_C_constant,
true);
107 if(symbol_table.
add(array_symbol))
108 throw "failed to add constarray symbol to symbol table";
110 const symbol_exprt array_expr = array_symbol.symbol_expr();
114 const std::size_t data_nb = jls_struct.component_number(
"data");
115 literal_init.operands()[data_nb] = array_pointer;
119 escaped_symbol_name_with_prefix +
"_return_value",
typet{}, ID_java};
120 return_symbol.base_name = escaped_symbol_name +
"_return_value";
121 return_symbol.pretty_name =
122 escaped_symbol_name.length() > 10
123 ? escaped_symbol_name.substr(0, 10) +
"..._return_value"
124 : escaped_symbol_name +
"_return_value";
125 return_symbol.is_lvalue =
true;
126 return_symbol.is_static_lifetime =
true;
127 return_symbol.is_state_var =
true;
129 ID_cprover_associate_array_to_pointer_func,
130 {array_symbol.value, array_pointer},
133 return_symbol.
type = return_symbol.value.type();
134 return_symbol.type.
set(ID_C_constant,
true);
135 if(symbol_table.
add(return_symbol))
136 throw "failed to add return symbol to symbol table";
142 exprt init_comma_expr(ID_comma);
143 init_comma_expr.
type() = literal_init.type();
145 return_symbol.symbol_expr(), std::move(literal_init));
146 new_symbol.value = init_comma_expr;
148 else if(jls_struct.components().size()>=1 &&
149 jls_struct.components()[0].get_name()==
"@java.lang.Object")
154 struct_exprt literal_init({std::move(jlo_init)}, new_symbol.type);
155 for(
const auto &comp : jls_struct.components())
157 if(comp.get_name()==
"@java.lang.Object")
165 literal_init.copy_to_operands(*init);
167 new_symbol.value = literal_init;
173 new_symbol.value = jlo_init;
174 new_symbol.value.type() = string_type;
177 bool add_failed = symbol_table.
add(new_symbol);
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();