Add unit tests on final status of fields

Author: thomasspriggs

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 \

jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.class

@@ -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;
+}

jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.java

@@ -0,0 +1,41 @@
+/*******************************************************************\
+
+ Module: Unit tests for converting fields
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <java-testing-utils/load_java_class.h>
+#include <java_bytecode/java_bytecode_convert_class.h>
+#include <java_bytecode/java_bytecode_parse_tree.h>
+#include <java_bytecode/java_types.h>
+#include <testing-utils/catch.hpp>
+
+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());
+      }
+    }
+  }
+}