Parse and convert the synthetic flag of java methods

For use in a downstream repository. This is used to indicate whether a
method was synthesized by the java compiler, as opposed to being a
method which has corresponding user written java code.

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -343,6 +343,7 @@ void java_bytecode_convert_method_lazy(
     member_type.set(ID_is_static, true);
   member_type.set_native(m.is_native);
   member_type.set_is_varargs(m.is_varargs);
+  member_type.set_is_synthetic(m.is_synthetic);
 
   if(m.is_bridge)
     member_type.set(ID_is_bridge_method, m.is_bridge);

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -85,7 +85,7 @@ struct java_bytecode_parse_treet
   {
     irep_idt base_name;
     bool is_native = false, is_abstract = false, is_synchronized = false,
-         is_bridge = false, is_varargs = false;
+         is_bridge = false, is_varargs = false, is_synthetic = false;
     source_locationt source_location;
 
     typedef std::vector<instructiont> instructionst;

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1864,6 +1864,7 @@ void java_bytecode_parsert::rmethod(classt &parsed_class)
   method.is_native=(access_flags&ACC_NATIVE)!=0;
   method.is_bridge = (access_flags & ACC_BRIDGE) != 0;
   method.is_varargs = (access_flags & ACC_VARARGS) != 0;
+  method.is_synthetic = (access_flags & ACC_SYNTHETIC) != 0;
   method.name=pool_entry(name_index).s;
   method.base_name=pool_entry(name_index).s;
   method.descriptor=id2string(pool_entry(descriptor_index).s);

jbmc/src/java_bytecode/java_types.h

@@ -393,6 +393,16 @@ public:
   {
     set(ID_is_varargs_method, is_varargs);
   }
+
+  bool is_synthetic() const
+  {
+    return get_bool(ID_synthetic);
+  }
+
+  void set_is_synthetic(bool is_synthetic)
+  {
+    set(ID_synthetic, is_synthetic);
+  }
 };
 
 template <>

jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithSyntheticMethod.java

@@ -0,0 +1,11 @@
+public class ClassWithSyntheticMethod {
+  private static int inaccessible() {
+    return 42;
+  }
+
+  public class Inner {
+    public int access() {
+      return inaccessible();
+    }
+  }
+}

jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp

@@ -249,3 +249,40 @@ SCENARIO(
     }
   }
 }
+
+SCENARIO(
+  "java_bytecode_convert_synthetic_method",
+  "[core][java_bytecode][java_bytecode_convert_method]")
+{
+  GIVEN("A class with a synthetic method.")
+  {
+    const symbol_tablet symbol_table = load_java_class(
+      "ClassWithSyntheticMethod",
+      "./java_bytecode/java_bytecode_convert_method");
+
+    WHEN("Parsing a synthetic method.")
+    {
+      const java_method_typet *const synthetic_method =
+        type_try_dynamic_cast<java_method_typet>(symbol_table.lookup_ref(
+          "java::ClassWithSyntheticMethod.access$000:()I").type);
+      REQUIRE(synthetic_method);
+
+      THEN("The method should be marked as synthetic.")
+      {
+        REQUIRE(synthetic_method->is_synthetic());
+      }
+    }
+    WHEN("Parsing a non synthetic method.")
+    {
+      const java_method_typet *const non_synthetic_method =
+        type_try_dynamic_cast<java_method_typet>(symbol_table.lookup_ref(
+          "java::ClassWithSyntheticMethod.inaccessible:()I").type);
+      REQUIRE(non_synthetic_method);
+
+      THEN("The method should not be marked as synthetic.")
+      {
+        REQUIRE(!non_synthetic_method->is_synthetic());
+      }
+    }
+  }
+}