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 \