Skip to content

Commit 751c040

Browse files
Simplify check whether String model is present
1 parent 8f2a82e commit 751c040

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -683,7 +683,8 @@ static bool add_nondet_string_pointer_initialization(
683683
const struct_typet &struct_type =
684684
to_struct_type(ns.follow(to_symbol_type(obj.type())));
685685

686-
if(!struct_type.has_component("data") || !struct_type.has_component("length"))
686+
// if no String model is loaded then we cannot construct a String object
687+
if(struct_type.get_bool(ID_incomplete_class))
687688
return true;
688689

689690
const exprt malloc_site = allocate_dynamic_object_with_decl(
@@ -868,8 +869,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
868869

869870
// Alternatively, if this is a void* we *must* initialise with null:
870871
// (This can currently happen for some cases of #exception_value)
871-
bool must_be_null=
872-
subtype==empty_typet();
872+
bool must_be_null = subtype == empty_typet();
873873

874874
if(must_be_null)
875875
{

0 commit comments

Comments
 (0)