Skip to content

Commit e23b4b1

Browse files
Add function_id parameter to add_pointer_to_array_association
This is in preparation for giving the function name to the function generating fresh java symbols.
1 parent ddf175e commit e23b4b1

File tree

3 files changed

+6
-3
lines changed

3 files changed

+6
-3
lines changed

jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -476,7 +476,7 @@ void initialize_nondet_string_fields(
476476
index_exprt(data_expr, from_integer(0, java_int_type())));
477477

478478
add_pointer_to_array_association(
479-
array_pointer, data_expr, symbol_table, loc, code);
479+
array_pointer, data_expr, symbol_table, loc, function_id, code);
480480

481481
add_array_to_length_association(
482482
data_expr, length_expr, symbol_table, loc, code);

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -478,7 +478,7 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
478478
char_array, array_typet(java_char_type(), infinity_exprt(java_int_type())));
479479

480480
add_pointer_to_array_association(
481-
string_expr.content(), inf_array, symbol_table, loc, code);
481+
string_expr.content(), inf_array, symbol_table, loc, function_id, code);
482482

483483
return string_expr;
484484
}
@@ -564,7 +564,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
564564
index_exprt(nondet_array_expr, from_integer(0, java_int_type())));
565565

566566
add_pointer_to_array_association(
567-
array_pointer, nondet_array_expr, symbol_table, loc, code);
567+
array_pointer, nondet_array_expr, symbol_table, loc, function_id, code);
568568

569569
add_array_to_length_association(
570570
nondet_array_expr, str.length(), symbol_table, loc, code);
@@ -677,12 +677,14 @@ exprt make_nondet_infinite_char_array(
677677
/// \param array: a character array expression
678678
/// \param symbol_table: the symbol table
679679
/// \param loc: source location
680+
/// \param function_id: name of the function in which the code will be added
680681
/// \param [out] code: code block to which declaration and calls get added
681682
void add_pointer_to_array_association(
682683
const exprt &pointer,
683684
const exprt &array,
684685
symbol_table_baset &symbol_table,
685686
const source_locationt &loc,
687+
const irep_idt &function_id,
686688
code_blockt &code)
687689
{
688690
PRECONDITION(array.type().id() == ID_array);

jbmc/src/java_bytecode/java_string_library_preprocess.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -353,6 +353,7 @@ void add_pointer_to_array_association(
353353
const exprt &array,
354354
symbol_table_baset &symbol_table,
355355
const source_locationt &loc,
356+
const irep_idt &function_id,
356357
code_blockt &code);
357358

358359
void add_array_to_length_association(

0 commit comments

Comments
 (0)