Skip to content

Commit dda09d1

Browse files
author
Joel Allred
authored
Merge pull request #3868 from allredj/typo-nondet-bool-array
Improve documentation in gen_nondet_array_init
2 parents 306fbf7 + aeef996 commit dda09d1

File tree

1 file changed

+5
-5
lines changed

1 file changed

+5
-5
lines changed

jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1426,7 +1426,7 @@ void java_object_factoryt::gen_nondet_array_init(
14261426

14271427
if(element_type.id() == ID_pointer || element_type.id() == ID_c_bool)
14281428
{
1429-
// For arrays of non-primitive types, nondeterministically initialize each
1429+
// For arrays of non-primitive type, nondeterministically initialize each
14301430
// element of the array
14311431
array_loop_init_code(
14321432
assignments,
@@ -1440,10 +1440,10 @@ void java_object_factoryt::gen_nondet_array_init(
14401440
}
14411441
else
14421442
{
1443-
// Arrays of primitive types can be initialized with a single instruction
1444-
// We don't do this for arrays of Booleans, because Bools are represented
1445-
// as bytes, so each cell must be initialized in a particular way (see
1446-
// gen_nondet_init).
1443+
// Arrays of primitive type can be initialized with a single instruction.
1444+
// We don't do this for arrays of primitive booleans, because booleans are
1445+
// represented as unsigned bytes, so each cell must be initialized as
1446+
// 0 or 1 (see gen_nondet_init).
14471447
array_primitive_init_code(
14481448
assignments,
14491449
init_array_expr,

0 commit comments

Comments
 (0)