diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
index cff74f57fb31..0f62f1534f3e 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -1033,6 +1033,32 @@ 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
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_class.h
index 3693290491f4..6fad2c8c17af 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.h
+++ b/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);
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.class
new file mode 100644
index 000000000000..e24c8e688967
Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.class differ
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.java b/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.java
new file mode 100644
index 000000000000..3bc08c8de171
--- /dev/null
+++ b/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithClassAnnotation.java
@@ -0,0 +1,3 @@
+@MyClassAnnotation(6)
+public class ClassWithClassAnnotation {
+}
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithMethodAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithMethodAnnotation.class
new file mode 100644
index 000000000000..4d3c00d3b06c
Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithMethodAnnotation.class differ
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithMethodAnnotation.java b/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithMethodAnnotation.java
new file mode 100644
index 000000000000..2efe9cc6cf40
--- /dev/null
+++ b/jbmc/unit/java_bytecode/java_bytecode_convert_class/ClassWithMethodAnnotation.java
@@ -0,0 +1,7 @@
+public class ClassWithMethodAnnotation {
+
+    @MyMethodAnnotation(methodValue = 11)
+    public void myMethod() {
+    }
+
+}
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyClassAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyClassAnnotation.class
new file mode 100644
index 000000000000..09977233041a
Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyClassAnnotation.class differ
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyClassAnnotation.java b/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyClassAnnotation.java
new file mode 100644
index 000000000000..2e9ece03aead
--- /dev/null
+++ b/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyClassAnnotation.java
@@ -0,0 +1,3 @@
+public @interface MyClassAnnotation {
+    int value();
+}
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyMethodAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyMethodAnnotation.class
new file mode 100644
index 000000000000..7c9b3a732855
Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyMethodAnnotation.class differ
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyMethodAnnotation.java b/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyMethodAnnotation.java
new file mode 100644
index 000000000000..9aa2e0be0e0a
--- /dev/null
+++ b/jbmc/unit/java_bytecode/java_bytecode_convert_class/MyMethodAnnotation.java
@@ -0,0 +1,3 @@
+public @interface MyMethodAnnotation {
+    int methodValue();
+}
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp
new file mode 100644
index 000000000000..5f69109e26af
--- /dev/null
+++ b/jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp
@@ -0,0 +1,75 @@
+/*******************************************************************\
+
+ Module: Unit tests for converting annotations
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+#include <java-testing-utils/load_java_class.h>
+#include <java_bytecode/java_types.h>
+#include <java_bytecode/java_bytecode_parse_tree.h>
+#include <java_bytecode/java_bytecode_convert_class.h>
+
+SCENARIO(
+  "java_bytecode_convert_annotations",
+  "[core][java_bytecode][java_bytecode_convert_class]")
+{
+  GIVEN("Some class files in the class path")
+  {
+    WHEN("Parsing a class with a class-level annotation")
+    {
+      const symbol_tablet &new_symbol_table = load_java_class(
+        "ClassWithClassAnnotation", "./java_bytecode/convert_java_annotations");
+
+      THEN("The annotation should have the correct structure")
+      {
+        const symbolt &class_symbol =
+          *new_symbol_table.lookup("java::ClassWithClassAnnotation");
+        const std::vector<java_annotationt> &java_annotations =
+          to_annotated_type(class_symbol.type).get_annotations();
+        java_bytecode_parse_treet::annotationst annotations;
+        convert_java_annotations(java_annotations, annotations);
+        REQUIRE(annotations.size() == 1);
+        const auto &annotation = annotations.front();
+        const auto &identifier =
+          to_symbol_type(annotation.type.subtype()).get_identifier();
+        REQUIRE(id2string(identifier) == "java::MyClassAnnotation");
+        const auto &element_value_pair = annotation.element_value_pairs.front();
+        const auto &element_name = element_value_pair.element_name;
+        REQUIRE(id2string(element_name) == "value");
+        const auto &expr = element_value_pair.value;
+        const auto comp_expr = from_integer(6, java_int_type());
+        REQUIRE(expr == comp_expr);
+      }
+    }
+    WHEN("Parsing a class with a method-level annotation")
+    {
+      const symbol_tablet &new_symbol_table = load_java_class(
+        "ClassWithMethodAnnotation",
+        "./java_bytecode/convert_java_annotations");
+
+      THEN("The annotation should have the correct structure")
+      {
+        const symbolt &method_symbol = *new_symbol_table.lookup(
+          "java::ClassWithMethodAnnotation.myMethod:()V");
+        const std::vector<java_annotationt> &java_annotations =
+          to_annotated_type(method_symbol.type).get_annotations();
+        java_bytecode_parse_treet::annotationst annotations;
+        convert_java_annotations(java_annotations, annotations);
+        REQUIRE(annotations.size() == 1);
+        const auto &annotation = annotations.front();
+        const auto &identifier =
+          to_symbol_type(annotation.type.subtype()).get_identifier();
+        REQUIRE(id2string(identifier) == "java::MyMethodAnnotation");
+        const auto &element_value_pair = annotation.element_value_pairs.front();
+        const auto &element_name = element_value_pair.element_name;
+        REQUIRE(id2string(element_name) == "methodValue");
+        const auto &expr = element_value_pair.value;
+        const auto &comp_expr = from_integer(11, java_int_type());
+        REQUIRE(expr == comp_expr);
+      }
+    }
+  }
+}