Skip to content

Commit 5045c4d

Browse files
romainbrenguierPetr Bauch
authored and
Petr Bauch
committed
Adapt unit tests for improved string allocation
1 parent f22d1eb commit 5045c4d

File tree

1 file changed

+6
-8
lines changed

1 file changed

+6
-8
lines changed

jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -84,22 +84,20 @@ SCENARIO(
8484
"tmp_object_factory = NONDET(int);",
8585
CPROVER_PREFIX "assume(tmp_object_factory >= 0);",
8686
CPROVER_PREFIX "assume(tmp_object_factory <= 20);",
87-
"char (*string_data_pointer)[INFINITY()];",
88-
"string_data_pointer = "
87+
"char (*nondet_infinite_array_pointer)[INFINITY()];",
88+
"nondet_infinite_array_pointer = "
8989
"ALLOCATE(char [INFINITY()], INFINITY(), false);",
90-
"char nondet_infinite_array[INFINITY()];",
91-
"nondet_infinite_array = NONDET(char [INFINITY()]);",
92-
"*string_data_pointer = nondet_infinite_array;",
90+
"*nondet_infinite_array_pointer = NONDET(char [INFINITY()]);",
9391
"int return_array;",
9492
"return_array = cprover_associate_array_to_pointer_func"
95-
"(*string_data_pointer, *string_data_pointer);",
93+
"(*nondet_infinite_array_pointer, *nondet_infinite_array_pointer);",
9694
"int return_array;",
9795
"return_array = cprover_associate_length_to_array_func"
98-
"(*string_data_pointer, tmp_object_factory);",
96+
"(*nondet_infinite_array_pointer, tmp_object_factory);",
9997
"arg = { [email protected]={ .@class_identifier"
10098
"=\"java::java.lang.String\" },"
10199
" .length=tmp_object_factory, "
102-
".data=*string_data_pointer };"};
100+
".data=*nondet_infinite_array_pointer };"};
103101
// clang-format on
104102

105103
for(std::size_t i = 0;

0 commit comments

Comments
 (0)