Skip to content

Commit db00d72

Browse files
Add function_id parameter to add_array_to_length_association
This is in preparation to giving the function_id to the function generating fresh java symbols.
1 parent e23b4b1 commit db00d72

File tree

3 files changed

+5
-2
lines changed

3 files changed

+5
-2
lines changed

jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -479,7 +479,7 @@ void initialize_nondet_string_fields(
479479
array_pointer, data_expr, symbol_table, loc, function_id, code);
480480

481481
add_array_to_length_association(
482-
data_expr, length_expr, symbol_table, loc, code);
482+
data_expr, length_expr, symbol_table, loc, function_id, code);
483483

484484
struct_expr.operands()[struct_type.component_number("data")] = array_pointer;
485485

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -567,7 +567,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
567567
array_pointer, nondet_array_expr, symbol_table, loc, function_id, code);
568568

569569
add_array_to_length_association(
570-
nondet_array_expr, str.length(), symbol_table, loc, code);
570+
nondet_array_expr, str.length(), symbol_table, loc, function_id, code);
571571

572572
code.add(code_assignt(str.content(), array_pointer), loc);
573573

@@ -713,12 +713,14 @@ void add_pointer_to_array_association(
713713
/// \param length: integer expression
714714
/// \param symbol_table: the symbol table
715715
/// \param loc: source location
716+
/// \param function_id: name of the function in which the code will be added
716717
/// \param [out] code: code block to which declaration and calls get added
717718
void add_array_to_length_association(
718719
const exprt &array,
719720
const exprt &length,
720721
symbol_table_baset &symbol_table,
721722
const source_locationt &loc,
723+
const irep_idt &function_id,
722724
code_blockt &code)
723725
{
724726
const symbolt &return_sym = get_fresh_aux_symbol(

jbmc/src/java_bytecode/java_string_library_preprocess.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -361,6 +361,7 @@ void add_array_to_length_association(
361361
const exprt &length,
362362
symbol_table_baset &symbol_table,
363363
const source_locationt &loc,
364+
const irep_idt &function_id,
364365
code_blockt &code);
365366

366367
void add_character_set_constraint(

0 commit comments

Comments
 (0)