Skip to content

Commit 8e92362

Browse files
Propagate string-printable option in object_factory
Note that for now this the default in the parameters is false and this is not affected yet by the command line options.
1 parent ae5f32e commit 8e92362

File tree

4 files changed

+10
-3
lines changed

4 files changed

+10
-3
lines changed

src/java_bytecode/java_bytecode_language.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,9 @@ struct object_factory_parameterst final
7575
/// dereference a pointer using a 'depth counter'. We set a pointer to null if
7676
/// such depth becomes >= than this maximum value.
7777
size_t max_nondet_tree_depth=MAX_NONDET_TREE_DEPTH;
78+
79+
/// Force string content to be ASCII printable characters when set to true.
80+
bool string_printable = false;
7881
};
7982

8083
typedef std::pair<

src/java_bytecode/java_object_factory.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -624,6 +624,7 @@ codet initialize_nondet_string_struct(
624624
/// content and association of its address to the pointer `expr`.
625625
/// \param expr: pointer to be affected
626626
/// \param max_nondet_string_length: maximum length of strings to initialize
627+
/// \param printable: Boolean, true to force content to be printable
627628
/// \param symbol_table: the symbol table
628629
/// \param loc: location in the source
629630
/// \param [out] code: code block in which initialization code is added
@@ -633,6 +634,7 @@ codet initialize_nondet_string_struct(
633634
static bool add_nondet_string_pointer_initialization(
634635
const exprt &expr,
635636
const std::size_t &max_nondet_string_length,
637+
bool printable,
636638
symbol_tablet &symbol_table,
637639
const source_locationt &loc,
638640
code_blockt &code)
@@ -652,7 +654,8 @@ static bool add_nondet_string_pointer_initialization(
652654
dereference_exprt(expr, struct_type),
653655
max_nondet_string_length,
654656
loc,
655-
symbol_table));
657+
symbol_table,
658+
printable));
656659
return false;
657660
}
658661

@@ -792,6 +795,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
792795
add_nondet_string_pointer_initialization(
793796
expr,
794797
object_factory_parameters.max_nondet_string_length,
798+
object_factory_parameters.string_printable,
795799
symbol_table,
796800
loc,
797801
assignments);

src/java_bytecode/java_object_factory.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -157,6 +157,6 @@ codet initialize_nondet_string_struct(
157157
const std::size_t &max_nondet_string_length,
158158
const source_locationt &loc,
159159
symbol_tablet &symbol_table,
160-
bool printable = false);
160+
bool printable);
161161

162162
#endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H

unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ SCENARIO(
4949
WHEN("Initialisation code for a string is generated")
5050
{
5151
const codet code =
52-
initialize_nondet_string_struct(expr, 20, loc, symbol_table);
52+
initialize_nondet_string_struct(expr, 20, loc, symbol_table, false);
5353

5454
THEN("Code is produced")
5555
{

0 commit comments

Comments
 (0)