From aeef99610565a24da6bb3b95075f3c8fdcdd6c54 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Mon, 21 Jan 2019 15:29:39 +0000 Subject: [PATCH] Improve documentation in gen_nondet_array_init Remove ambiguity between primitive boolean and Boolean objects. --- jbmc/src/java_bytecode/java_object_factory.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 1ee14c5ee54..0c8d2b7cf0b 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -1426,7 +1426,7 @@ void java_object_factoryt::gen_nondet_array_init( if(element_type.id() == ID_pointer || element_type.id() == ID_c_bool) { - // For arrays of non-primitive types, nondeterministically initialize each + // For arrays of non-primitive type, nondeterministically initialize each // element of the array array_loop_init_code( assignments, @@ -1440,10 +1440,10 @@ void java_object_factoryt::gen_nondet_array_init( } else { - // Arrays of primitive types can be initialized with a single instruction - // We don't do this for arrays of Booleans, because Bools are represented - // as bytes, so each cell must be initialized in a particular way (see - // gen_nondet_init). + // Arrays of primitive type can be initialized with a single instruction. + // We don't do this for arrays of primitive booleans, because booleans are + // represented as unsigned bytes, so each cell must be initialized as + // 0 or 1 (see gen_nondet_init). array_primitive_init_code( assignments, init_array_expr,