Skip to content

Commit 5a9e977

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 ec7092e commit 5a9e977

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
@@ -487,11 +487,13 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
487487
/// given type
488488
/// \param type: a type for refined strings
489489
/// \param loc: a location in the program
490+
/// \param function_id: name of the function in which the code will be added
490491
/// \param symbol_table: symbol table
491492
/// \return a new symbol
492493
symbol_exprt java_string_library_preprocesst::fresh_string(
493494
const typet &type,
494495
const source_locationt &loc,
496+
const irep_idt &function_id,
495497
symbol_table_baset &symbol_table)
496498
{
497499
symbolt string_symbol=get_fresh_aux_symbol(
@@ -588,7 +590,7 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
588590
symbol_table_baset &symbol_table,
589591
code_blockt &code)
590592
{
591-
const exprt str = fresh_string(type, loc, symbol_table);
593+
const exprt str = fresh_string(type, loc, function_id, symbol_table);
592594

593595
allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
594596

jbmc/src/java_bytecode/java_string_library_preprocess.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -227,6 +227,7 @@ class java_string_library_preprocesst:public messaget
227227
symbol_exprt fresh_string(
228228
const typet &type,
229229
const source_locationt &loc,
230+
const irep_idt &function_id,
230231
symbol_table_baset &symbol_table);
231232

232233
symbol_exprt fresh_array(

0 commit comments

Comments
 (0)