diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 306df0a0ef6..15277d84ddb 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -753,6 +753,8 @@ void java_bytecode_convert_classt::convert( else component.set_access(ID_default); + component.set_is_final(f.is_final); + // Load annotations if(!f.annotations.empty()) { diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 5bf5f13742e..2c57d8008e5 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -38,6 +38,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \ java_bytecode/java_bytecode_parser/parse_java_annotations.cpp \ java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \ java_bytecode/java_bytecode_parser/parse_java_class.cpp \ + java_bytecode/java_bytecode_parser/parse_java_field.cpp \ java_bytecode/java_object_factory/gen_nondet_string_init.cpp \ java_bytecode/java_replace_nondet/replace_nondet.cpp \ java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.class new file mode 100644 index 00000000000..b11af28caa0 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.java b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.java new file mode 100644 index 00000000000..70719cb1654 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.java @@ -0,0 +1,10 @@ + +class ClassWithFields { + final boolean final1 = true; + final Boolean final2 = false; + final Object final3 = null; + + boolean nonFinal1 = true; + Boolean nonFinal2 = false; + Object nonFinal3 = null; +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_field.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_field.cpp new file mode 100644 index 00000000000..4faab4915e0 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_field.cpp @@ -0,0 +1,41 @@ +/*******************************************************************\ + + Module: Unit tests for converting fields + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include +#include +#include + +SCENARIO( + "java_bytecode_parse_field", + "[core][java_bytecode][java_bytecode_parser]") +{ + GIVEN("Some class with final and non final fields") + { + const symbol_tablet &symbol_table = load_java_class( + "ClassWithFields", "./java_bytecode/java_bytecode_parser"); + + WHEN("Parsing the class file structure") + { + THEN("The the final status of the classes fields should be correct.") + { + const symbolt &class_symbol = + symbol_table.lookup_ref("java::ClassWithFields"); + const java_class_typet &java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_component("final1").get_is_final()); + REQUIRE(java_class.get_component("final2").get_is_final()); + REQUIRE(java_class.get_component("final3").get_is_final()); + REQUIRE(!java_class.get_component("nonFinal1").get_is_final()); + REQUIRE(!java_class.get_component("nonFinal1").get_is_final()); + REQUIRE(!java_class.get_component("nonFinal1").get_is_final()); + } + } + } +} diff --git a/src/util/std_types.h b/src/util/std_types.h index 487fde2e51b..a100de8c08f 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -189,6 +189,16 @@ class struct_union_typet:public typet { return set(ID_C_is_padding, is_padding); } + + bool get_is_final() const + { + return get_bool(ID_final); + } + + void set_is_final(const bool is_final) + { + set(ID_final, is_final); + } }; typedef std::vector componentst;