Skip to content

Commit 6c58e38

Browse files
Add function_id parameter to add_character_set_constraint
This is in preparation for using a new fresh_java_symbol function which takes a function_id as parameter.
1 parent c21dfa5 commit 6c58e38

File tree

3 files changed

+3
-1
lines changed

3 files changed

+3
-1
lines changed

jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -487,7 +487,7 @@ void initialize_nondet_string_fields(
487487
if(printable)
488488
{
489489
add_character_set_constraint(
490-
array_pointer, length_expr, " -~", symbol_table, loc, code);
490+
array_pointer, length_expr, " -~", symbol_table, loc, function_id, code);
491491
}
492492
}
493493

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -702,6 +702,7 @@ void add_character_set_constraint(
702702
const irep_idt &char_set,
703703
symbol_table_baset &symbol_table,
704704
const source_locationt &loc,
705+
const irep_idt &function_id,
705706
code_blockt &code)
706707
{
707708
PRECONDITION(pointer.type().id() == ID_pointer);

jbmc/src/java_bytecode/java_string_library_preprocess.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -360,6 +360,7 @@ void add_character_set_constraint(
360360
const irep_idt &char_set,
361361
symbol_table_baset &symbol_table,
362362
const source_locationt &loc,
363+
const irep_idt &function_id,
363364
code_blockt &code);
364365

365366
#endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H

0 commit comments

Comments
 (0)