Skip to content

Commit 06f89d9

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 d3f768c commit 06f89d9

File tree

3 files changed

+4
-1
lines changed

3 files changed

+4
-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: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -695,13 +695,15 @@ void add_array_to_length_association(
695695
/// lower case ascii letters.
696696
/// \param symbol_table: the symbol table
697697
/// \param loc: source location
698+
/// \param function_id: the name of the function
698699
/// \param [out] code: code block to which declaration and calls get added
699700
void add_character_set_constraint(
700701
const exprt &pointer,
701702
const exprt &length,
702703
const irep_idt &char_set,
703704
symbol_table_baset &symbol_table,
704705
const source_locationt &loc,
706+
const irep_idt &function_id,
705707
code_blockt &code)
706708
{
707709
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
@@ -361,6 +361,7 @@ void add_character_set_constraint(
361361
const irep_idt &char_set,
362362
symbol_table_baset &symbol_table,
363363
const source_locationt &loc,
364+
const irep_idt &function_id,
364365
code_blockt &code);
365366

366367
#endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H

0 commit comments

Comments
 (0)