Skip to content

Commit dc13905

Browse files
Delete unused function fresh_array
This function is not used, there is no point in keeping it.
1 parent db00d72 commit dc13905

File tree

2 files changed

+0
-26
lines changed

2 files changed

+0
-26
lines changed

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 0 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -241,27 +241,6 @@ void java_string_library_preprocesst::add_string_type(
241241
string_symbol->mode = ID_java;
242242
}
243243

244-
/// add a symbol in the table with static lifetime and name containing
245-
/// `cprover_string_array` and given type
246-
/// \param type: an array type
247-
/// \param location: a location in the program
248-
/// \param symbol_table: symbol table
249-
symbol_exprt java_string_library_preprocesst::fresh_array(
250-
const typet &type,
251-
const source_locationt &location,
252-
symbol_tablet &symbol_table)
253-
{
254-
symbolt array_symbol=get_fresh_aux_symbol(
255-
type,
256-
"cprover_string_array",
257-
"cprover_string_array",
258-
location,
259-
ID_java,
260-
symbol_table);
261-
array_symbol.is_static_lifetime=true;
262-
return array_symbol.symbol_expr();
263-
}
264-
265244
/// calls string_refine_preprocesst::process_operands with a list of parameters.
266245
/// \param params: a list of function parameters
267246
/// \param loc: location in the source

jbmc/src/java_bytecode/java_string_library_preprocess.h

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -229,11 +229,6 @@ class java_string_library_preprocesst:public messaget
229229
const source_locationt &loc,
230230
symbol_table_baset &symbol_table);
231231

232-
symbol_exprt fresh_array(
233-
const typet &type,
234-
const source_locationt &loc,
235-
symbol_tablet &symbol_table);
236-
237232
refined_string_exprt decl_string_expr(
238233
const source_locationt &loc,
239234
const irep_idt &function_id,

0 commit comments

Comments
 (0)