diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
index 3e415f4f85d..cfd5363473d 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
+++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
@@ -98,6 +98,14 @@ struct java_bytecode_parse_treet
       return instructions.back();
     }
 
+    /// Java annotations that were applied to parameters of this method
+    /// \remarks Each element in the vector corresponds to the annotations on
+    /// the parameter of this method with the matching index. A parameter that
+    /// does not have annotations can have an entry in this vector that is an
+    /// empty annotationst. Trailing parameters that have no annotations may be
+    /// entirely omitted from this vector.
+    std::vector<annotationst> parameter_annotations;
+
     struct exceptiont
     {
       exceptiont()
diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index 45e8f51e76a..4e201ad7439 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -1243,6 +1243,21 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
   {
     rRuntimeAnnotation_attribute(method.annotations);
   }
+  else if(
+    attribute_name == "RuntimeInvisibleParameterAnnotations" ||
+    attribute_name == "RuntimeVisibleParameterAnnotations")
+  {
+    u1 parameter_count = read_u1();
+    // There may be attributes for both runtime-visiible and rutime-invisible
+    // annotations, the length of either array may be longer than the other as
+    // trailing parameters without annotations are omitted.
+    // Extend our parameter_annotations if this one is longer than the one
+    // previously recorded (if any).
+    if(method.parameter_annotations.size() < parameter_count)
+      method.parameter_annotations.resize(parameter_count);
+    for(u2 param_no = 0; param_no < parameter_count; ++param_no)
+      rRuntimeAnnotation_attribute(method.parameter_annotations[param_no]);
+  }
   else if(attribute_name == "Exceptions")
   {
     method.throws_exception_table = rexceptions_attribute();
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationsEverywhere.class b/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationsEverywhere.class
new file mode 100644
index 00000000000..2fa38719f19
Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationsEverywhere.class differ
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationsEverywhere.java b/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationsEverywhere.java
new file mode 100644
index 00000000000..a8a5079321f
--- /dev/null
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationsEverywhere.java
@@ -0,0 +1,43 @@
+@interface ClassAnnotation {
+}
+
+@java.lang.annotation.Retention(java.lang.annotation.RetentionPolicy.RUNTIME)
+@interface RuntimeClassAnnotation {
+}
+
+@interface FieldAnnotation {
+}
+
+@java.lang.annotation.Retention(java.lang.annotation.RetentionPolicy.RUNTIME)
+@interface RuntimeFieldAnnotation {
+}
+
+@interface MethodAnnotation {
+}
+
+@java.lang.annotation.Retention(java.lang.annotation.RetentionPolicy.RUNTIME)
+@interface RuntimeMethodAnnotation {
+}
+
+@interface ParameterAnnotation {
+}
+
+@java.lang.annotation.Retention(java.lang.annotation.RetentionPolicy.RUNTIME)
+@interface RuntimeParameterAnnotation {
+}
+
+@ClassAnnotation
+@RuntimeClassAnnotation
+public class AnnotationsEverywhere {
+    @FieldAnnotation
+    @RuntimeFieldAnnotation
+    public int x;
+
+    @MethodAnnotation
+    @RuntimeMethodAnnotation
+    public void foo(
+        @RuntimeParameterAnnotation int p,
+        @ParameterAnnotation int q)
+    {
+    }
+}
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ClassAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassAnnotation.class
new file mode 100644
index 00000000000..3c843eb339f
Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassAnnotation.class differ
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/FieldAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_parser/FieldAnnotation.class
new file mode 100644
index 00000000000..314037e960c
Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/FieldAnnotation.class differ
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/MethodAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_parser/MethodAnnotation.class
new file mode 100644
index 00000000000..d363b8b760d
Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/MethodAnnotation.class differ
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ParameterAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ParameterAnnotation.class
new file mode 100644
index 00000000000..f2658a8611d
Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ParameterAnnotation.class differ
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/RuntimeClassAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_parser/RuntimeClassAnnotation.class
new file mode 100644
index 00000000000..f1843334eb8
Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/RuntimeClassAnnotation.class differ
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/RuntimeFieldAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_parser/RuntimeFieldAnnotation.class
new file mode 100644
index 00000000000..35f5dc99fb6
Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/RuntimeFieldAnnotation.class differ
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/RuntimeMethodAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_parser/RuntimeMethodAnnotation.class
new file mode 100644
index 00000000000..f4e55e97d20
Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/RuntimeMethodAnnotation.class differ
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/RuntimeParameterAnnotation.class b/jbmc/unit/java_bytecode/java_bytecode_parser/RuntimeParameterAnnotation.class
new file mode 100644
index 00000000000..9164d68a1ec
Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/RuntimeParameterAnnotation.class differ
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
index aaac5ca4ac8..81f448c2e1c 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
@@ -7,10 +7,60 @@
 \*******************************************************************/
 
 #include <java-testing-utils/load_java_class.h>
+#include <java-testing-utils/require_type.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>
+#include <testing-utils/free_form_cmdline.h>
+#include <testing-utils/message.h>
+
+class test_java_bytecode_languaget : public java_bytecode_languaget
+{
+public:
+  std::vector<irep_idt> get_parsed_class_names()
+  {
+    std::vector<irep_idt> parsed_class_names;
+    for(const auto &named_class
+      : java_class_loader.get_class_with_overlays_map())
+    {
+      parsed_class_names.push_back(named_class.first);
+    }
+    return parsed_class_names;
+  }
+
+  java_class_loadert::parse_tree_with_overlayst &get_parse_trees_for_class(
+    const irep_idt &class_name)
+  {
+    return java_class_loader.get_class_with_overlays_map().at(class_name);
+  }
+};
+
+static irep_idt get_base_name(const typet &type)
+{
+  return type.get(ID_C_base_name);
+}
+
+static void require_matching_annotations(
+  const java_bytecode_parse_treet::annotationst &annotations,
+  std::vector<irep_idt> expected_annotations)
+{
+  std::vector<irep_idt> annotation_names;
+  std::transform(
+    annotations.begin(),
+    annotations.end(),
+    std::back_inserter(annotation_names),
+    [](const java_bytecode_parse_treet::annotationt &annotation)
+    {
+      return get_base_name(
+        require_type::require_pointer(annotation.type, {}).subtype());
+    });
+  std::sort(annotation_names.begin(), annotation_names.end());
+  std::sort(expected_annotations.begin(), expected_annotations.end());
+  REQUIRE_THAT(
+    annotation_names,
+    Catch::Matchers::Equals(expected_annotations));
+}
 
 // See
 // https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1
@@ -116,5 +166,66 @@ SCENARIO(
         REQUIRE(id2string(another_dave) == "Another Dave");
       }
     }
+    WHEN("Parsing a class with annotations everywhere")
+    {
+      free_form_cmdlinet command_line;
+      command_line.add_flag("no-lazy-methods");
+      command_line.add_flag("no-refine-strings");
+      test_java_bytecode_languaget language;
+      language.set_message_handler(null_message_handler);
+      language.get_language_options(command_line);
+
+      std::istringstream java_code_stream("ignored");
+      language.parse(java_code_stream, "AnnotationsEverywhere.class");
+      const java_class_loadert::parse_tree_with_overlayst &parse_trees =
+        language.get_parse_trees_for_class("AnnotationsEverywhere");
+      REQUIRE(parse_trees.size() == 1);
+      const java_bytecode_parse_treet::classt &parsed_class =
+        parse_trees.front().parsed_class;
+
+      THEN("Only the correct annotations should be on the class")
+      {
+        require_matching_annotations(
+          parsed_class.annotations,
+          { "ClassAnnotation", "RuntimeClassAnnotation" });
+      }
+
+      THEN("Only the correct annotations should be on the field")
+      {
+        REQUIRE(parsed_class.fields.size() == 1);
+        const java_bytecode_parse_treet::fieldt &field =
+          parsed_class.fields.front();
+        require_matching_annotations(
+          field.annotations, { "FieldAnnotation", "RuntimeFieldAnnotation" });
+      }
+
+      auto method_it = std::find_if(
+        parsed_class.methods.begin(),
+        parsed_class.methods.end(),
+        [](const java_bytecode_parse_treet::methodt &method)
+        {
+          return method.name == "foo";
+        });
+      REQUIRE(method_it != parsed_class.methods.end());
+      const java_bytecode_parse_treet::methodt &method = *method_it;
+
+      THEN("Only the correct annotations should be on the method")
+      {
+        require_matching_annotations(
+          method.annotations,
+          { "MethodAnnotation", "RuntimeMethodAnnotation" });
+      }
+
+      THEN("Only the correct annotations should be on the parameter")
+      {
+        REQUIRE(method.parameter_annotations.size() == 2);
+        require_matching_annotations(
+          method.parameter_annotations[0],
+          { "RuntimeParameterAnnotation" });
+        require_matching_annotations(
+          method.parameter_annotations[1],
+          { "ParameterAnnotation" });
+      }
+    }
   }
 }