Add tag for java_method_type

Author: jeannielynnmoulton

jbmc/src/java_bytecode/java_types.h

@@ -245,9 +245,35 @@ inline bool can_cast_type<java_class_typet>(const typet &type)
 class java_method_typet : public code_typet
 {
 public:
-  using code_typet::parametert;
   using code_typet::parameterst;
-  using code_typet::code_typet;
+  using code_typet::parametert;
+
+  /// Constructs a new code type, i.e. function type
+  /// \param _parameters: the vector of function parameters
+  /// \param _return_type: the return type
+  java_method_typet(parameterst &&_parameters, typet &&_return_type)
+  {
+    set(ID_C_java_method_type, true);
+    parameters().swap(_parameters);
+    return_type().swap(_return_type);
+  }
+
+  /// Constructs a new code type, i.e. function type
+  /// \param _parameters: the vector of function parameters
+  /// \param _return_type: the return type
+  java_method_typet(parameterst &&_parameters, const typet &_return_type)
+  {
+    set(ID_C_java_method_type, true);
+    parameters().swap(_parameters);
+    return_type() = _return_type;
+  }
+
+  /// \deprecated
+  DEPRECATED("Use the two argument constructor instead")
+  java_method_typet()
+  {
+    set(ID_C_java_method_type, true);
+  }
 
   const std::vector<irep_idt> throws_exceptions() const
   {

src/util/irep_ids.def

@@ -695,6 +695,7 @@ IREP_ID_ONE(r_ok)
 IREP_ID_ONE(w_ok)
 IREP_ID_ONE(super_class)
 IREP_ID_ONE(exceptions_thrown_list)
+IREP_ID_TWO(C_java_method_type, #java_method_type)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree