Generalize and rename does_annotation_exist

Making the function return an optionalt instead of a boolean provides
some additional functionality without adding much complexity to the
existing code that calls it.

Author: antlechner

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -875,8 +875,9 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
 
 bool java_bytecode_convert_classt::is_overlay_method(const methodt &method)
 {
-  return java_bytecode_parse_treet::does_annotation_exist(
-    method.annotations, ID_overlay_method);
+  return java_bytecode_parse_treet::find_annotation(
+           method.annotations, ID_overlay_method)
+    .has_value();
 }
 
 bool java_bytecode_convert_class(

jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp

@@ -121,23 +121,30 @@ void java_bytecode_parse_treet::annotationt::element_value_pairt::output(
   out << expr2java(value, ns);
 }
 
-bool java_bytecode_parse_treet::does_annotation_exist(
+/// Find an annotation given its name
+/// \param annotations: A vector of annotationt
+/// \param annotation_type_name: An irep_idt representing the name of the
+///   annotation class, e.g. java::java.lang.SuppressWarnings
+/// \return The first annotation with the given name in annotations if one
+///    exists, an empty optionalt otherwise.
+optionalt<java_bytecode_parse_treet::annotationt>
+java_bytecode_parse_treet::find_annotation(
   const annotationst &annotations,
   const irep_idt &annotation_type_name)
 {
-  return
-    std::find_if(
-      annotations.begin(),
-      annotations.end(),
-      [&annotation_type_name](const annotationt &annotation)
-      {
-        if(annotation.type.id() != ID_pointer)
-          return false;
-        typet type = annotation.type.subtype();
-        return
-          type.id() == ID_symbol
-          && to_symbol_type(type).get_identifier() == annotation_type_name;
-      }) != annotations.end();
+  const auto annotation_it = std::find_if(
+    annotations.begin(),
+    annotations.end(),
+    [&annotation_type_name](const annotationt &annotation) {
+      if(annotation.type.id() != ID_pointer)
+        return false;
+      const typet &type = annotation.type.subtype();
+      return type.id() == ID_symbol &&
+             to_symbol_type(type).get_identifier() == annotation_type_name;
+    });
+  if(annotation_it == annotations.end())
+    return {};
+  return *annotation_it;
 }
 
 void java_bytecode_parse_treet::methodt::output(std::ostream &out) const

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -44,7 +44,7 @@ class java_bytecode_parse_treet
 
   typedef std::vector<annotationt> annotationst;
 
-  static bool does_annotation_exist(
+  static optionalt<annotationt> find_annotation(
     const annotationst &annotations,
     const irep_idt &annotation_type_name);
 

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -106,8 +106,9 @@ optionalt<java_bytecode_parse_treet> java_class_loadert::get_class_from_jar(
 
 static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
 {
-  return java_bytecode_parse_treet::does_annotation_exist(
-    c.annotations, ID_overlay_class);
+  return java_bytecode_parse_treet::find_annotation(
+           c.annotations, ID_overlay_class)
+    .has_value();
 }
 
 /// Check through all the places class parse trees can appear and returns the