Skip to content

Commit 89c123e

Browse files
Adapt unit test for allocation of string data
1 parent 2e760b3 commit 89c123e

File tree

1 file changed

+9
-5
lines changed

1 file changed

+9
-5
lines changed

unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -70,18 +70,22 @@ SCENARIO(
7070
"tmp_object_factory = NONDET(int);",
7171
"__CPROVER_assume(tmp_object_factory >= 0);",
7272
"__CPROVER_assume(tmp_object_factory <= 20);",
73+
"char (*string_data_pointer)[INFINITY()];",
74+
"string_data_pointer = "
75+
"ALLOCATE(char [INFINITY()], INFINITY(), false);",
7376
"char nondet_infinite_array[INFINITY()];",
7477
"nondet_infinite_array = NONDET(char [INFINITY()]);",
78+
"*string_data_pointer = nondet_infinite_array;",
7579
"int return_array;",
7680
"return_array = cprover_associate_array_to_pointer_func"
77-
"(nondet_infinite_array, nondet_infinite_array);",
81+
"(*string_data_pointer, *string_data_pointer);",
7882
"int return_array;",
7983
"return_array = cprover_associate_length_to_array_func"
80-
"(nondet_infinite_array, tmp_object_factory);",
84+
"(*string_data_pointer, tmp_object_factory);",
8185
"arg = { [email protected]={ .@class_identifier"
82-
"=\"java::java.lang.String\", .@lock=false },"
83-
" .length=tmp_object_factory, "
84-
".data=nondet_infinite_array };"};
86+
"=\"java::java.lang.String\", .@lock=false },"
87+
" .length=tmp_object_factory, "
88+
".data=*string_data_pointer };"};
8589

8690
for(std::size_t i = 0;
8791
i < code_string.size() && i < reference_code.size();

0 commit comments

Comments
 (0)