Skip to content

Commit 71526e3

Browse files
Add function_name parameter to fresh_string
This is in preparation to giving the function_name to the function generating fresh java symbols.
1 parent a11ccc4 commit 71526e3

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
@@ -488,11 +488,13 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
488488
/// given type
489489
/// \param type: a type for refined strings
490490
/// \param loc: a location in the program
491+
/// \param function_name: name of the function in which the code will be added
491492
/// \param symbol_table: symbol table
492493
/// \return a new symbol
493494
symbol_exprt java_string_library_preprocesst::fresh_string(
494495
const typet &type,
495496
const source_locationt &loc,
497+
const irep_idt &function_name,
496498
symbol_table_baset &symbol_table)
497499
{
498500
symbolt string_symbol=get_fresh_aux_symbol(
@@ -589,7 +591,7 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
589591
symbol_table_baset &symbol_table,
590592
code_blockt &code)
591593
{
592-
const exprt str = fresh_string(type, loc, symbol_table);
594+
const exprt str = fresh_string(type, loc, function_id, symbol_table);
593595

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

jbmc/src/java_bytecode/java_string_library_preprocess.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -224,6 +224,7 @@ class java_string_library_preprocesst:public messaget
224224
symbol_exprt fresh_string(
225225
const typet &type,
226226
const source_locationt &loc,
227+
const irep_idt &function_name,
227228
symbol_table_baset &symbol_table);
228229

229230
symbol_exprt fresh_array(

0 commit comments

Comments
 (0)