Add can_cast_type and precondition.

Also removes an irrelevant unit test due to this change.

Author: jeannielynnmoulton

jbmc/src/java_bytecode/java_types.h

@@ -284,16 +284,21 @@ class java_method_typet : public code_typet
   }
 };
 
+template<>
+inline bool can_cast_type<java_method_typet>(const typet &type)
+{
+  return type.id() == ID_code && type.get_bool(ID_C_java_method_type);
+}
+
 inline const java_method_typet &to_java_method_type(const typet &type)
 {
-  PRECONDITION(type.id() == ID_code);
+  PRECONDITION(can_cast_type<java_method_typet>(type));
   return static_cast<const java_method_typet &>(type);
 }
 
 inline java_method_typet &to_java_method_type(typet &type)
 {
-  PRECONDITION(type.id() == ID_code);
-  type.set(ID_C_java_method_type, true);
+  PRECONDITION(can_cast_type<java_method_typet>(type));
   return static_cast<java_method_typet &>(type);
 }
 

jbmc/unit/Makefile

@@ -21,7 +21,6 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
        java_bytecode/java_types/erase_type_arguments.cpp \
        java_bytecode/java_types/generic_type_index.cpp \
        java_bytecode/java_types/java_generic_symbol_type.cpp \
-       java_bytecode/java_types/java_method_type.cpp \
        java_bytecode/java_types/java_type_from_string.cpp \
        java_bytecode/java_utils_test.cpp \
        java_bytecode/load_method_by_regex.cpp \

jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp

@@ -30,8 +30,12 @@ SCENARIO(
         symbol_table.lookup_ref(method_name + ":(Ljava/lang/Object;)I");
 
       const java_method_typet &function_type =
-        require_type::require_code(function_symbol.type);
-      THEN("The method should be marked as a bridge method")
+        require_type::require_java_method(function_symbol.type);
+      THEN("The method symbol should be of java_method_typet")
+      {
+        REQUIRE(function_type.get_bool(ID_C_java_method_type));
+      }
+      THEN("And the method should be marked as a bridge method")
       {
         REQUIRE(function_type.get_bool(ID_is_bridge_method));
       }