Define inverse function of convert_annotations

This function can be used to retrieve annotations from a symbol table. A
unit test is added for this functionality.

Author: antlechner

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -1032,6 +1032,31 @@ void convert_annotations(
   }
 }
 
+/// Convert java annotations, e.g. as retrieved from the symbol table, back
+/// to type annotationt (inverse of convert_annotations())
+/// \param java_annotations: The java_annotationt collection to convert
+/// \param annotations: The annotationt collection to populate
+void convert_java_annotations(
+  const std::vector<java_annotationt> &java_annotations,
+  java_bytecode_parse_treet::annotationst &annotations)
+{
+  for(const auto &java_annotation : java_annotations)
+  {
+    annotations.emplace_back(java_bytecode_parse_treet::annotationt());
+    auto &annotation = annotations.back();
+    annotation.type = java_annotation.get_type();
+
+    std::transform(
+      java_annotation.get_values().begin(),
+      java_annotation.get_values().end(),
+      std::back_inserter(annotation.element_value_pairs),
+      [](const java_annotationt::valuet &value)
+        -> java_bytecode_parse_treet::annotationt::element_value_pairt {
+          return {value.get_name(), value.get_value()};
+        });
+  }
+}
+
 /// Checks if the class is implicitly generic, i.e., it is an inner class of
 /// any generic class. All uses of the implicit generic type parameters within
 /// the inner class are updated to point to the type parameters of the

jbmc/src/java_bytecode/java_bytecode_convert_class.h

@@ -33,6 +33,10 @@ void convert_annotations(
   const java_bytecode_parse_treet::annotationst &parsed_annotations,
   std::vector<java_annotationt> &annotations);
 
+void convert_java_annotations(
+  const std::vector<java_annotationt> &java_annotations,
+  java_bytecode_parse_treet::annotationst &annotations);
+
 void mark_java_implicitly_generic_class_type(
   const irep_idt &class_name,
   symbol_tablet &symbol_table);

jbmc/unit/Makefile

@@ -9,6 +9,7 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
        java_bytecode/goto-programs/class_hierarchy_graph.cpp \
        java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp \
        java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \
+       java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp \
        java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \
        java_bytecode/java_object_factory/gen_nondet_string_init.cpp \

jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.class

@@ -0,0 +1,3 @@
+@MyClassAnnotation(6)
+public class ClassWithClassAnnotation {
+}

jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.java

@@ -0,0 +1,7 @@
+public class ClassWithMethodAnnotation {
+
+    @MyMethodAnnotation(methodValue = 11)
+    public void myMethod() {
+    }
+
+}

jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithMethodAnnotation.class

@@ -0,0 +1,3 @@
+public @interface MyClassAnnotation {
+    int value();
+}