diff --git a/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/src/java_bytecode/java_bytecode_typecheck_expr.cpp index e5b4d0fe572..9ebe8a61324 100644 --- a/src/java_bytecode/java_bytecode_typecheck_expr.cpp +++ b/src/java_bytecode/java_bytecode_typecheck_expr.cpp @@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_pointer_casts.h" #include "java_types.h" #include "java_utils.h" +#include "java_root_class.h" void java_bytecode_typecheckt::typecheck_expr(exprt &expr) { @@ -134,15 +135,7 @@ void java_bytecode_typecheckt::typecheck_expr_java_string_literal(exprt &expr) const auto &jlo_struct=to_struct_type(ns.follow(jlo_symbol)); struct_exprt jlo_init(jlo_symbol); const auto &jls_struct=to_struct_type(ns.follow(string_type)); - - jlo_init.copy_to_operands( - constant_exprt( - "java::java.lang.String", - jlo_struct.components()[0].type())); - jlo_init.copy_to_operands( - from_integer( - 0, - jlo_struct.components()[1].type())); + java_root_class_init(jlo_init, jlo_struct, false, "java::java.lang.String"); // If string refinement *is* around, populate the actual // contents as well: diff --git a/src/java_bytecode/java_root_class.cpp b/src/java_bytecode/java_root_class.cpp index f3353c48d1a..cbeec3ff40d 100644 --- a/src/java_bytecode/java_root_class.cpp +++ b/src/java_bytecode/java_root_class.cpp @@ -8,8 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_root_class.h" +#include #include -#include #include "java_types.h" @@ -52,3 +52,26 @@ void java_root_class(symbolt &class_symbol) components.insert(components.begin(), component); } } + +/// Adds members for an object of the root class (usually java.lang.Object). +/// \param jlo [out] : object to initialize +/// \param root_type: type of the root class +/// \param lock: lock field +/// \param class_identifier: class identifier field +void java_root_class_init( + struct_exprt &jlo, + const struct_typet &root_type, + const bool lock, + const irep_idt &class_identifier) +{ + jlo.operands().resize(root_type.components().size()); + + const std::size_t clsid_nb=root_type.component_number("@class_identifier"); + const typet &clsid_type=root_type.components()[clsid_nb].type(); + constant_exprt clsid(class_identifier, clsid_type); + jlo.operands()[clsid_nb]=clsid; + + const std::size_t lock_nb=root_type.component_number("@lock"); + const typet &lock_type=root_type.components()[lock_nb].type(); + jlo.operands()[lock_nb]=from_integer(lock, lock_type); +} diff --git a/src/java_bytecode/java_root_class.h b/src/java_bytecode/java_root_class.h index fcdb11333db..583556de857 100644 --- a/src/java_bytecode/java_root_class.h +++ b/src/java_bytecode/java_root_class.h @@ -18,4 +18,10 @@ Author: Daniel Kroening, kroening@kroening.com void java_root_class( class symbolt &class_symbol); +void java_root_class_init( + struct_exprt &jlo, + const struct_typet &root_type, + bool lock, + const irep_idt &class_identifier); + #endif // CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H