Skip to content

Commit e9725d3

Browse files
Add function_id parameter to fresh_string
This is in preparation to giving the function_id to the function generating fresh java symbols.
1 parent 775fa44 commit e9725d3

File tree

2 files changed

+4
-1
lines changed

2 files changed

+4
-1
lines changed

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -430,11 +430,13 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
430430
/// given type
431431
/// \param type: a type for refined strings
432432
/// \param loc: a location in the program
433+
/// \param function_id: name of the function in which the code will be added
433434
/// \param symbol_table: symbol table
434435
/// \return a new symbol
435436
symbol_exprt java_string_library_preprocesst::fresh_string(
436437
const typet &type,
437438
const source_locationt &loc,
439+
const irep_idt &function_id,
438440
symbol_table_baset &symbol_table)
439441
{
440442
symbolt string_symbol=get_fresh_aux_symbol(
@@ -531,7 +533,7 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
531533
symbol_table_baset &symbol_table,
532534
code_blockt &code)
533535
{
534-
const exprt str = fresh_string(type, loc, symbol_table);
536+
const exprt str = fresh_string(type, loc, function_id, symbol_table);
535537

536538
allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
537539

jbmc/src/java_bytecode/java_string_library_preprocess.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -221,6 +221,7 @@ class java_string_library_preprocesst:public messaget
221221
symbol_exprt fresh_string(
222222
const typet &type,
223223
const source_locationt &loc,
224+
const irep_idt &function_id,
224225
symbol_table_baset &symbol_table);
225226

226227
refined_string_exprt decl_string_expr(

0 commit comments

Comments
 (0)