Merge pull request #2976 from thomasspriggs/tas/final_fields

 Store the final status of fields in `componentt`

Author: Thomas Kiley

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())
     {

jbmc/unit/Makefile

@@ -39,6 +39,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());
+      }
+    }
+  }
+}

jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_field.cpp

@@ -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<componentt> componentst;