Add to_annotated_type and enable type_checked_cast for annotated_typet

Author: NathanJPhillips

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -467,7 +467,7 @@ void java_bytecode_convert_classt::convert(
     {
       convert_annotations(
         f.annotations,
-        static_cast<annotated_typet &>(new_symbol.type).get_annotations());
+        type_checked_cast<annotated_typet>(new_symbol.type).get_annotations());
     }
 
     // Do we have the static field symbol already?

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -392,7 +392,7 @@ void java_bytecode_convert_method_lazy(
   {
     convert_annotations(
       m.annotations,
-      static_cast<annotated_typet &>(static_cast<typet &>(member_type))
+      type_checked_cast<annotated_typet>(static_cast<typet &>(member_type))
         .get_annotations());
   }
 

src/java_bytecode/java_qualifiers.cpp

@@ -47,8 +47,7 @@ void java_qualifierst::read(const typet &src)
 void java_qualifierst::write(typet &src) const
 {
   c_qualifierst::write(src);
-  auto &annotated_type = static_cast<annotated_typet &>(src);
-  annotated_type.get_annotations() = annotations;
+  type_checked_cast<annotated_typet>(src).get_annotations() = annotations;
 }
 
 qualifierst &java_qualifierst::operator+=(const qualifierst &other)

src/java_bytecode/java_types.h

@@ -82,6 +82,22 @@ class annotated_typet : public typet
   }
 };
 
+inline const annotated_typet &to_annotated_type(const typet &type)
+{
+  return static_cast<const annotated_typet &>(type);
+}
+
+inline annotated_typet &to_annotated_type(typet &type)
+{
+  return static_cast<annotated_typet &>(type);
+}
+
+template <>
+inline bool can_cast_type<annotated_typet>(const typet &type)
+{
+  return true;
+}
+
 class java_class_typet:public class_typet
 {
  public:
@@ -129,7 +145,7 @@ class java_class_typet:public class_typet
 
   std::vector<java_annotationt> &get_annotations()
   {
-    return static_cast<annotated_typet &>(
+    return type_checked_cast<annotated_typet>(
       static_cast<typet &>(*this)).get_annotations();
   }
 };