diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp
index 18be0320498..dd7a161e303 100644
--- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp
+++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp
@@ -376,7 +376,7 @@ void ci_lazy_methodst::initialize_instantiated_classes(
   for(const auto &mname : entry_points)
   {
     const auto &symbol=ns.lookup(mname);
-    const auto &mtype=to_code_type(symbol.type);
+    const auto &mtype = to_java_method_type(symbol.type);
     for(const auto &param : mtype.parameters())
     {
       if(param.type().id()==ID_pointer)
diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp
index 69518dd1c45..edd196ff53a 100644
--- a/jbmc/src/java_bytecode/expr2java.cpp
+++ b/jbmc/src/java_bytecode/expr2java.cpp
@@ -56,11 +56,10 @@ std::string expr2javat::convert_code_function_call(
     dest+='=';
   }
 
-  const code_typet &code_type=
-    to_code_type(src.function().type());
+  const java_method_typet &method_type =
+    to_java_method_type(src.function().type());
 
-  bool has_this=code_type.has_this() &&
-                !src.arguments().empty();
+  bool has_this = method_type.has_this() && !src.arguments().empty();
 
   if(has_this)
   {
@@ -284,7 +283,7 @@ std::string expr2javat::convert_rec(
     return q+"byte"+d;
   else if(src.id()==ID_code)
   {
-    const code_typet &code_type=to_code_type(src);
+    const java_method_typet &method_type = to_java_method_type(src);
 
     // Java doesn't really have syntax for function types,
     // so we make one up, loosely inspired by the syntax
@@ -293,11 +292,10 @@ std::string expr2javat::convert_rec(
     std::string dest="";
 
     dest+='(';
-    const code_typet::parameterst &parameters=code_type.parameters();
+    const java_method_typet::parameterst &parameters = method_type.parameters();
 
-    for(code_typet::parameterst::const_iterator
-        it=parameters.begin();
-        it!=parameters.end();
+    for(java_method_typet::parameterst::const_iterator it = parameters.begin();
+        it != parameters.end();
         it++)
     {
       if(it!=parameters.begin())
@@ -306,7 +304,7 @@ std::string expr2javat::convert_rec(
       dest+=convert(it->type());
     }
 
-    if(code_type.has_ellipsis())
+    if(method_type.has_ellipsis())
     {
       if(!parameters.empty())
         dest+=", ";
@@ -315,7 +313,7 @@ std::string expr2javat::convert_rec(
 
     dest+=')';
 
-    const typet &return_type=code_type.return_type();
+    const typet &return_type = method_type.return_type();
     dest+=" -> "+convert(return_type);
 
     return q + dest;
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
index 3c85b9c7401..e92d1906167 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -781,12 +781,12 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
 
     const irep_idt clone_name=
       id2string(symbol_type_identifier)+".clone:()Ljava/lang/Object;";
-    code_typet::parametert this_param;
+    java_method_typet::parametert this_param;
     this_param.set_identifier(id2string(clone_name)+"::this");
     this_param.set_base_name("this");
     this_param.set_this();
     this_param.type()=java_reference_type(symbol_type);
-    const code_typet clone_type({this_param}, java_lang_object_type());
+    const java_method_typet clone_type({this_param}, java_lang_object_type());
 
     parameter_symbolt this_symbol;
     this_symbol.name=this_param.get_identifier();
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index 21cac212cd4..69f30186d15 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -87,11 +87,11 @@ class patternt
 ///   parameters, which are initially nameless as method conversion hasn't
 ///   happened. Also creates symbols in `symbol_table`.
 static void assign_parameter_names(
-  code_typet &ftype,
+  java_method_typet &ftype,
   const irep_idt &name_prefix,
   symbol_table_baset &symbol_table)
 {
-  code_typet::parameterst &parameters=ftype.parameters();
+  java_method_typet::parameterst &parameters = ftype.parameters();
 
   // Mostly borrowed from java_bytecode_convert.cpp; maybe factor this out.
   // assign names to parameters
@@ -255,7 +255,7 @@ const exprt java_bytecode_convert_methodt::variable(
 ///   message handler to collect warnings
 /// \return
 ///   the constructed member type
-code_typet member_type_lazy(
+java_method_typet member_type_lazy(
   const std::string &descriptor,
   const optionalt<std::string> &signature,
   const std::string &class_name,
@@ -282,10 +282,11 @@ code_typet member_type_lazy(
         signature.value(),
         class_name);
       INVARIANT(member_type_from_signature.id()==ID_code, "Must be code type");
-      if(to_code_type(member_type_from_signature).parameters().size()==
-         to_code_type(member_type_from_descriptor).parameters().size())
+      if(
+        to_java_method_type(member_type_from_signature).parameters().size() ==
+        to_java_method_type(member_type_from_descriptor).parameters().size())
       {
-        return to_code_type(member_type_from_signature);
+        return to_java_method_type(member_type_from_signature);
       }
       else
       {
@@ -306,7 +307,7 @@ code_typet member_type_lazy(
                         << message.eom;
     }
   }
-  return to_code_type(member_type_from_descriptor);
+  return to_java_method_type(member_type_from_descriptor);
 }
 
 /// Retrieves the symbol of the lambda method associated with the given
@@ -345,7 +346,7 @@ void java_bytecode_convert_method_lazy(
 {
   symbolt method_symbol;
 
-  code_typet member_type = member_type_lazy(
+  java_method_typet member_type = member_type_lazy(
     m.descriptor,
     m.signature,
     id2string(class_symbol.name),
@@ -378,8 +379,8 @@ void java_bytecode_convert_method_lazy(
   // do we need to add 'this' as a parameter?
   if(!m.is_static)
   {
-    code_typet::parameterst &parameters = member_type.parameters();
-    code_typet::parametert this_p;
+    java_method_typet::parameterst &parameters = member_type.parameters();
+    java_method_typet::parametert this_p;
     const reference_typet object_ref_type=
       java_reference_type(symbol_typet(class_symbol.name));
     this_p.type()=object_ref_type;
@@ -442,12 +443,12 @@ void java_bytecode_convert_methodt::convert(
 
   symbolt &method_symbol=*symbol_table.get_writeable(method_identifier);
 
-  // Obtain a std::vector of code_typet::parametert objects from the
+  // Obtain a std::vector of java_method_typet::parametert objects from the
   // (function) type of the symbol
   java_method_typet method_type = to_java_method_type(method_symbol.type);
   method_type.set(ID_C_class, class_symbol.name);
   method_return_type = method_type.return_type();
-  code_typet::parameterst &parameters = method_type.parameters();
+  java_method_typet::parameterst &parameters = method_type.parameters();
 
   // Determine the number of local variable slots used by the JVM to maintain
   // the formal parameters
@@ -1250,9 +1251,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
             id2string(arg0.get(ID_identifier))==
             "java::org.cprover.CProver.assume:(Z)V")
     {
-      const code_typet &code_type=to_code_type(arg0.type());
-      INVARIANT(code_type.parameters().size()==1,
-                "function expected to have exactly one parameter");
+      const java_method_typet &method_type = to_java_method_type(arg0.type());
+      INVARIANT(
+        method_type.parameters().size() == 1,
+        "function expected to have exactly one parameter");
       c = replace_call_to_cprover_assume(i_it->source_location, c);
     }
     // replace calls to CProver.atomicBegin
@@ -1995,8 +1997,8 @@ codet java_bytecode_convert_methodt::convert_monitorenterexit(
     return code_skipt();
 
   // becomes a function call
-  code_typet type(
-    {code_typet::parametert(java_reference_type(void_typet()))},
+  java_method_typet type(
+    {java_method_typet::parametert(java_reference_type(void_typet()))},
     void_typet());
   code_function_callt call;
   call.function() = symbol_exprt(descriptor, type);
@@ -2105,8 +2107,8 @@ void java_bytecode_convert_methodt::convert_invoke(
   const bool is_virtual(
     statement == "invokevirtual" || statement == "invokeinterface");
 
-  code_typet &code_type = to_code_type(arg0.type());
-  code_typet::parameterst &parameters(code_type.parameters());
+  java_method_typet &method_type = to_java_method_type(arg0.type());
+  java_method_typet::parameterst &parameters(method_type.parameters());
 
   if(use_this)
   {
@@ -2122,13 +2124,13 @@ void java_bytecode_convert_methodt::convert_invoke(
         {
           if(needed_lazy_methods)
             needed_lazy_methods->add_needed_class(classname);
-          code_type.set_is_constructor();
+          method_type.set_is_constructor();
         }
         else
-          code_type.set(ID_java_super_method_call, true);
+          method_type.set(ID_java_super_method_call, true);
       }
       reference_typet object_ref_type = java_reference_type(thistype);
-      code_typet::parametert this_p(object_ref_type);
+      java_method_typet::parametert this_p(object_ref_type);
       this_p.set_this();
       this_p.set_base_name("this");
       parameters.insert(parameters.begin(), this_p);
@@ -2170,7 +2172,7 @@ void java_bytecode_convert_methodt::convert_invoke(
 
   // do some type adjustment for return values
 
-  const typet &return_type = code_type.return_type();
+  const typet &return_type = method_type.return_type();
 
   if(return_type.id() != ID_empty)
   {
@@ -2215,7 +2217,7 @@ void java_bytecode_convert_methodt::convert_invoke(
     symbol.value.make_nil();
     symbol.mode = ID_java;
     assign_parameter_names(
-      to_code_type(symbol.type), symbol.name, symbol_table);
+      to_java_method_type(symbol.type), symbol.name, symbol_table);
 
     debug() << "Generating codet:  new opaque symbol: method '" << symbol.name
             << "'" << eom;
@@ -2945,11 +2947,11 @@ optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
   const source_locationt &location,
   const exprt &arg0)
 {
-  const code_typet &code_type = to_code_type(arg0.type());
+  const java_method_typet &method_type = to_java_method_type(arg0.type());
 
   const optionalt<symbolt> &lambda_method_symbol = get_lambda_method_symbol(
     lambda_method_handles,
-    code_type.get_int(ID_java_lambda_method_handle_index));
+    method_type.get_int(ID_java_lambda_method_handle_index));
   if(lambda_method_symbol.has_value())
     debug() << "Converting invokedynamic for lambda: "
             << lambda_method_symbol.value().name << eom;
@@ -2958,11 +2960,11 @@ optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
                "type"
             << eom;
 
-  const code_typet::parameterst &parameters(code_type.parameters());
+  const java_method_typet::parameterst &parameters(method_type.parameters());
 
   pop(parameters.size());
 
-  const typet &return_type = code_type.return_type();
+  const typet &return_type = method_type.return_type();
 
   if(return_type.id() == ID_empty)
     return {};
@@ -3019,13 +3021,13 @@ void java_bytecode_initialize_parameter_names(
     &local_variable_table,
   symbol_table_baset &symbol_table)
 {
-  // Obtain a std::vector of code_typet::parametert objects from the
+  // Obtain a std::vector of java_method_typet::parametert objects from the
   // (function) type of the symbol
-  code_typet &code_type = to_code_type(method_symbol.type);
-  code_typet::parameterst &parameters = code_type.parameters();
+  java_method_typet &method_type = to_java_method_type(method_symbol.type);
+  java_method_typet::parameterst &parameters = method_type.parameters();
 
   // Find number of parameters
-  unsigned slots_for_parameters = java_method_parameter_slots(code_type);
+  unsigned slots_for_parameters = java_method_parameter_slots(method_type);
 
   // Find parameter names in the local variable table:
   typedef std::pair<irep_idt, irep_idt> base_name_and_identifiert;
diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
index 9eee6a4131d..ba6fcfd94ce 100644
--- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
@@ -446,8 +446,8 @@ void java_bytecode_instrumentt::instrument_code(codet &code)
     add_expr_instrumentation(block, code_function_call.lhs());
     add_expr_instrumentation(block, code_function_call.function());
 
-    const code_typet &function_type=
-      to_code_type(code_function_call.function().type());
+    const java_method_typet &function_type =
+      to_java_method_type(code_function_call.function().type());
 
     // Check for a null this-argument of a virtual call:
     if(function_type.has_this())
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
index a2cf076a131..8499e5913e6 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -1068,7 +1068,7 @@ bool java_bytecode_languaget::convert_single_method(
 
   // The return of an opaque function is a source of an otherwise invisible
   // instantiation, so here we ensure we've loaded the appropriate classes.
-  const code_typet function_type = to_code_type(symbol.type);
+  const java_method_typet function_type = to_java_method_type(symbol.type);
   if(
     const pointer_typet *pointer_return_type =
       type_try_dynamic_cast<pointer_typet>(function_type.return_type()))
diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index ef41a7366f4..2f77e62492b 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -610,7 +610,7 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src)
 {
   if(src.id()==ID_code)
   {
-    const code_typet &ct=to_code_type(src);
+    const java_method_typet &ct = to_java_method_type(src);
     const typet &rt=ct.return_type();
     get_class_refs_rec(rt);
     for(const auto &p : ct.parameters())
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck.h b/jbmc/src/java_bytecode/java_bytecode_typecheck.h
index 9ac5611539e..4d56e105bf8 100644
--- a/jbmc/src/java_bytecode/java_bytecode_typecheck.h
+++ b/jbmc/src/java_bytecode/java_bytecode_typecheck.h
@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H
 
+#include "java_types.h"
+
 #include <set>
 #include <map>
 
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp
index 2f26feb59bc..25f28713105 100644
--- a/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp
@@ -38,13 +38,14 @@ void java_bytecode_typecheckt::typecheck_type(typet &type)
   }
   else if(type.id()==ID_code)
   {
-    code_typet &code_type=to_code_type(type);
-    typecheck_type(code_type.return_type());
+    java_method_typet &method_type = to_java_method_type(type);
+    typecheck_type(method_type.return_type());
 
-    code_typet::parameterst &parameters=code_type.parameters();
+    java_method_typet::parameterst &parameters = method_type.parameters();
 
-    for(code_typet::parameterst::iterator
-        it=parameters.begin(); it!=parameters.end(); it++)
+    for(java_method_typet::parameterst::iterator it = parameters.begin();
+        it != parameters.end();
+        it++)
       typecheck_type(it->type());
   }
 }
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index 5d14e771bb5..73fadb9b697 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -36,7 +36,7 @@ static void create_initialize(symbol_table_baset &symbol_table)
   initialize.base_name=INITIALIZE_FUNCTION;
   initialize.mode=ID_java;
 
-  initialize.type = code_typet({}, empty_typet());
+  initialize.type = java_method_typet({}, empty_typet());
 
   code_blockt init_code;
 
@@ -251,12 +251,12 @@ static void java_static_lifetime_init(
 bool is_java_main(const symbolt &function)
 {
   bool named_main = has_suffix(id2string(function.name), JAVA_MAIN_METHOD);
-  const code_typet &function_type = to_code_type(function.type);
+  const java_method_typet &function_type = to_java_method_type(function.type);
   const typet &string_array_type = java_type_from_string("[Ljava/lang/String;");
   // checks whether the function is static and has a single String[] parameter
   bool is_static = !function_type.has_this();
   // this should be implied by the signature
-  const code_typet::parameterst &parameters = function_type.parameters();
+  const java_method_typet::parameterst &parameters = function_type.parameters();
   bool has_correct_type = function_type.return_type().id() == ID_empty &&
                           parameters.size() == 1 &&
                           parameters[0].type().full_eq(string_array_type);
@@ -281,8 +281,8 @@ exprt::operandst java_build_arguments(
   object_factory_parameterst object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
-  const code_typet::parameterst &parameters=
-    to_code_type(function.type).parameters();
+  const java_method_typet::parameterst &parameters =
+    to_java_method_type(function.type).parameters();
 
   exprt::operandst main_arguments;
   main_arguments.resize(parameters.size());
@@ -299,7 +299,7 @@ exprt::operandst java_build_arguments(
       param_number<parameters.size();
       param_number++)
   {
-    const code_typet::parametert &p=parameters[param_number];
+    const java_method_typet::parametert &p = parameters[param_number];
     const irep_idt base_name=p.get_base_name().empty()?
       ("argument#"+std::to_string(param_number)):p.get_base_name();
 
@@ -352,14 +352,14 @@ void java_record_outputs(
   code_blockt &init_code,
   symbol_table_baset &symbol_table)
 {
-  const code_typet::parameterst &parameters=
-    to_code_type(function.type).parameters();
+  const java_method_typet::parameterst &parameters =
+    to_java_method_type(function.type).parameters();
 
   exprt::operandst result;
   result.reserve(parameters.size()+1);
 
-  bool has_return_value=
-    to_code_type(function.type).return_type()!=empty_typet();
+  bool has_return_value =
+    to_java_method_type(function.type).return_type() != empty_typet();
 
   if(has_return_value)
   {
@@ -624,14 +624,14 @@ bool generate_java_start_function(
 
   // if the method return type is not void, store return value in a new variable
   // named 'return'
-  if(to_code_type(symbol.type).return_type()!=empty_typet())
+  if(to_java_method_type(symbol.type).return_type() != empty_typet())
   {
     auxiliary_symbolt return_symbol;
     return_symbol.mode=ID_java;
     return_symbol.is_static_lifetime=false;
     return_symbol.name=JAVA_ENTRY_POINT_RETURN_SYMBOL;
     return_symbol.base_name="return";
-    return_symbol.type=to_code_type(symbol.type).return_type();
+    return_symbol.type = to_java_method_type(symbol.type).return_type();
 
     symbol_table.add(return_symbol);
     call_main.lhs()=return_symbol.symbol_expr();
@@ -715,7 +715,7 @@ bool generate_java_start_function(
   symbolt new_symbol;
 
   new_symbol.name=goto_functionst::entry_point();
-  new_symbol.type = code_typet({}, empty_typet());
+  new_symbol.type = java_method_typet({}, empty_typet());
   new_symbol.value.swap(init_code);
   new_symbol.mode=ID_java;
 
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index d9461898a10..2760a9936bb 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -1084,7 +1084,7 @@ void java_object_factoryt::gen_nondet_struct_init(
 
   if(const auto func = symbol_table.lookup(init_method_name))
   {
-    const code_typet &type = to_code_type(func->type);
+    const java_method_typet &type = to_java_method_type(func->type);
     code_function_callt fun_call;
     fun_call.function() = func->symbol_expr();
     if(type.has_this())
diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp
index e486b38a9f3..b4daf706820 100644
--- a/jbmc/src/java_bytecode/java_static_initializers.cpp
+++ b/jbmc/src/java_bytecode/java_static_initializers.cpp
@@ -294,7 +294,7 @@ static void create_clinit_wrapper_symbols(
 
   // Create symbol for the "clinit_wrapper"
   symbolt wrapper_method_symbol;
-  const code_typet wrapper_method_type({}, void_typet());
+  const java_method_typet wrapper_method_type({}, void_typet());
   wrapper_method_symbol.name = clinit_wrapper_name(class_name);
   wrapper_method_symbol.pretty_name = wrapper_method_symbol.name;
   wrapper_method_symbol.base_name = "clinit_wrapper";
@@ -714,7 +714,7 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
       "a class cannot be both incomplete, and so have stub static fields, and "
       "also define a static initializer");
 
-    const code_typet thunk_type({}, void_typet());
+    const java_method_typet thunk_type({}, void_typet());
 
     symbolt static_init_symbol;
     static_init_symbol.name = static_init_name;
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 21bc0451e7a..8a2b0f634f4 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -280,7 +280,7 @@ symbol_exprt java_string_library_preprocesst::fresh_array(
 ///   added
 /// \return a list of expressions
 exprt::operandst java_string_library_preprocesst::process_parameters(
-  const code_typet::parameterst &params,
+  const java_method_typet::parameterst &params,
   const source_locationt &loc,
   symbol_table_baset &symbol_table,
   code_blockt &init_code)
@@ -956,7 +956,7 @@ java_string_library_preprocesst::string_literal_to_string_expr(
 ///   return false
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 codet java_string_library_preprocesst::make_equals_function_code(
-  const code_typet &type,
+  const java_method_typet &type,
   const source_locationt &loc,
   const irep_idt &function_id,
   symbol_table_baset &symbol_table)
@@ -1011,13 +1011,13 @@ codet java_string_library_preprocesst::make_equals_function_code(
 /// \param symbol_table: symbol table
 /// \return Code corresponding to the Java conversion of floats to strings.
 codet java_string_library_preprocesst::make_float_to_string_code(
-  const code_typet &type,
+  const java_method_typet &type,
   const source_locationt &loc,
   const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
   // Getting the argument
-  code_typet::parameterst params=type.parameters();
+  java_method_typet::parameterst params = type.parameters();
   PRECONDITION(params.size()==1);
   const symbol_exprt arg(params[0].get_identifier(), params[0].type());
 
@@ -1155,12 +1155,12 @@ codet java_string_library_preprocesst::make_float_to_string_code(
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 codet java_string_library_preprocesst::make_init_function_from_call(
   const irep_idt &function_name,
-  const code_typet &type,
+  const java_method_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table,
   bool ignore_first_arg)
 {
-  code_typet::parameterst params=type.parameters();
+  java_method_typet::parameterst params = type.parameters();
 
   // The first parameter is the object to be initialized
   PRECONDITION(!params.empty());
@@ -1196,12 +1196,12 @@ codet java_string_library_preprocesst::make_init_function_from_call(
 codet java_string_library_preprocesst::
   make_assign_and_return_function_from_call(
     const irep_idt &function_name,
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table)
 {
   // This is similar to assign functions except we return a pointer to `this`
-  code_typet::parameterst params=type.parameters();
+  java_method_typet::parameterst params = type.parameters();
   PRECONDITION(!params.empty());
   code_blockt code;
   code.add(
@@ -1221,7 +1221,7 @@ codet java_string_library_preprocesst::
 ///   name.
 codet java_string_library_preprocesst::make_assign_function_from_call(
   const irep_idt &function_name,
-  const code_typet &type,
+  const java_method_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table)
 {
@@ -1503,7 +1503,7 @@ exprt java_string_library_preprocesst::make_argument_for_format(
 ///         argument to the internal format function a structure containing
 ///         the different possible types.
 codet java_string_library_preprocesst::make_string_format_code(
-  const code_typet &type,
+  const java_method_typet &type,
   const source_locationt &loc,
   const irep_idt &function_id,
   symbol_table_baset &symbol_table)
@@ -1562,12 +1562,12 @@ codet java_string_library_preprocesst::make_string_format_code(
 /// return class1
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 codet java_string_library_preprocesst::make_object_get_class_code(
-  const code_typet &type,
+  const java_method_typet &type,
   const source_locationt &loc,
   const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
-  code_typet::parameterst params=type.parameters();
+  java_method_typet::parameterst params = type.parameters();
   const symbol_exprt this_obj(params[0].get_identifier(), params[0].type());
 
   // Code to be returned
@@ -1620,7 +1620,8 @@ codet java_string_library_preprocesst::make_object_get_class_code(
     "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;");
   fun_call.lhs()=class1;
   fun_call.arguments().push_back(string1);
-  const code_typet fun_type({code_typet::parametert(string_ptr_type)}, class_type);
+  const java_method_typet fun_type(
+    {java_method_typet::parametert(string_ptr_type)}, class_type);
   fun_call.function().type()=fun_type;
   code.add(fun_call, loc);
 
@@ -1641,7 +1642,7 @@ codet java_string_library_preprocesst::make_object_get_class_code(
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~
 codet java_string_library_preprocesst::make_function_from_call(
   const irep_idt &function_name,
-  const code_typet &type,
+  const java_method_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table)
 {
@@ -1670,7 +1671,7 @@ codet java_string_library_preprocesst::make_function_from_call(
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 codet java_string_library_preprocesst::make_string_returning_function_from_call(
   const irep_idt &function_name,
-  const code_typet &type,
+  const java_method_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table)
 {
@@ -1711,7 +1712,7 @@ codet java_string_library_preprocesst::make_string_returning_function_from_call(
 /// return str
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 codet java_string_library_preprocesst::make_copy_string_code(
-  const code_typet &type,
+  const java_method_typet &type,
   const source_locationt &loc,
   const irep_idt &function_id,
   symbol_table_baset &symbol_table)
@@ -1723,7 +1724,7 @@ codet java_string_library_preprocesst::make_copy_string_code(
   refined_string_exprt string_expr = decl_string_expr(loc, symbol_table, code);
 
   // Assign the argument to string_expr
-  code_typet::parametert op=type.parameters()[0];
+  java_method_typet::parametert op = type.parameters()[0];
   symbol_exprt arg0(op.get_identifier(), op.type());
   code_assign_java_string_to_string_expr(
     string_expr, arg0, loc, symbol_table, code);
@@ -1753,7 +1754,7 @@ codet java_string_library_preprocesst::make_copy_string_code(
 /// this = string_expr_to_java_string(string_expr)
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 codet java_string_library_preprocesst::make_copy_constructor_code(
-  const code_typet &type,
+  const java_method_typet &type,
   const source_locationt &loc,
   const irep_idt &function_id,
   symbol_table_baset &symbol_table)
@@ -1767,7 +1768,7 @@ codet java_string_library_preprocesst::make_copy_constructor_code(
   refined_string_exprt string_expr = decl_string_expr(loc, symbol_table, code);
 
   // Assign argument to a string_expr
-  code_typet::parameterst params=type.parameters();
+  java_method_typet::parameterst params = type.parameters();
   symbol_exprt arg1(params[1].get_identifier(), params[1].type());
   code_assign_java_string_to_string_expr(
     string_expr, arg1, loc, symbol_table, code);
@@ -1791,7 +1792,7 @@ codet java_string_library_preprocesst::make_copy_constructor_code(
 /// \return code implementing String intitialization from a char array and
 ///         arguments offset and end.
 codet java_string_library_preprocesst::make_init_from_array_code(
-  const code_typet &type,
+  const java_method_typet &type,
   const source_locationt &loc,
   const irep_idt &function_id,
   symbol_table_baset &symbol_table)
@@ -1801,7 +1802,7 @@ codet java_string_library_preprocesst::make_init_from_array_code(
   // Code for the output
   code_blockt code;
 
-  code_typet::parameterst params = type.parameters();
+  java_method_typet::parameterst params = type.parameters();
   PRECONDITION(params.size() == 4);
   exprt::operandst args =
     process_parameters(type.parameters(), loc, symbol_table, code);
@@ -1842,16 +1843,16 @@ codet java_string_library_preprocesst::make_init_from_array_code(
 /// return this->length
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 codet java_string_library_preprocesst::make_string_length_code(
-  const code_typet &type,
+  const java_method_typet &type,
   const source_locationt &loc,
   const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
   (void)function_id;
 
-  code_typet::parameterst params=type.parameters();
+  java_method_typet::parameterst params = type.parameters();
   symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
-  dereference_exprt deref=
+  dereference_exprt deref =
     checked_dereference(arg_this, arg_this.type().subtype());
   return code_returnt(get_length(deref, symbol_table));
 }
@@ -1902,7 +1903,7 @@ exprt java_string_library_preprocesst::code_for_function(
   symbol_table_baset &symbol_table)
 {
   const irep_idt &function_id = symbol.name;
-  const code_typet &type = to_code_type(symbol.type);
+  const java_method_typet &type = to_java_method_type(symbol.type);
   const source_locationt &loc = symbol.location;
   auto it_id=cprover_equivalent_to_java_function.find(function_id);
   if(it_id!=cprover_equivalent_to_java_function.end())
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
index 382dc1b5d9d..78c3ae4667f 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.h
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h
@@ -99,7 +99,7 @@ class java_string_library_preprocesst:public messaget
   const refined_string_typet refined_string_type;
 
   typedef std::function<codet(
-    const code_typet &,
+    const java_method_typet &,
     const source_locationt &,
     const irep_idt &,
     symbol_table_baset &)>
@@ -146,56 +146,56 @@ class java_string_library_preprocesst:public messaget
   std::unordered_set<irep_idt> string_types;
 
   codet make_equals_function_code(
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   codet make_float_to_string_code(
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   codet make_string_to_char_array_code(
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     const irep_idt &function_id,
     symbol_tablet &symbol_table);
 
   codet make_string_format_code(
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   codet make_copy_string_code(
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   codet make_copy_constructor_code(
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   codet make_string_length_code(
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   codet make_object_get_class_code(
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   // Helper functions
   exprt::operandst process_parameters(
-    const code_typet::parameterst &params,
+    const java_method_typet::parameterst &params,
     const source_locationt &loc,
     symbol_table_baset &symbol_table,
     code_blockt &init_code);
@@ -306,32 +306,32 @@ class java_string_library_preprocesst:public messaget
 
   codet make_function_from_call(
     const irep_idt &function_name,
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
   codet make_init_function_from_call(
     const irep_idt &function_name,
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table,
     bool ignore_first_arg = true);
 
   codet make_assign_and_return_function_from_call(
     const irep_idt &function_name,
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
   codet make_assign_function_from_call(
     const irep_idt &function_name,
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
   codet make_string_returning_function_from_call(
     const irep_idt &function_name,
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
@@ -354,7 +354,7 @@ class java_string_library_preprocesst:public messaget
   exprt get_object_at_index(const exprt &argv, std::size_t index);
 
   codet make_init_from_array_code(
-    const code_typet &type,
+    const java_method_typet &type,
     const source_locationt &loc,
     const irep_idt &function_id,
     symbol_table_baset &symbol_table);
diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp
index 67e3a27e971..2dd3c3f0178 100644
--- a/jbmc/src/java_bytecode/java_types.cpp
+++ b/jbmc/src/java_bytecode/java_types.cpp
@@ -542,14 +542,14 @@ typet java_type_from_string(
         parse_list_types(src.substr(0, e_pos + 1), class_name_prefix, '(', ')');
 
       // create parameters for each type
-      code_typet::parameterst parameters;
+      java_method_typet::parameterst parameters;
       std::transform(
         param_types.begin(),
         param_types.end(),
         std::back_inserter(parameters),
-        [](const typet &type) { return code_typet::parametert(type); });
+        [](const typet &type) { return java_method_typet::parametert(type); });
 
-      return code_typet(std::move(parameters), std::move(return_type));
+      return java_method_typet(std::move(parameters), std::move(return_type));
     }
 
   case '[': // array type
@@ -817,7 +817,7 @@ void get_dependencies_from_generic_parameters_rec(
   // method type with parameters and return value
   else if(t.id() == ID_code)
   {
-    const code_typet &c = to_code_type(t);
+    const java_method_typet &c = to_java_method_type(t);
     get_dependencies_from_generic_parameters_rec(c.return_type(), refs);
     for(const auto &param : c.parameters())
       get_dependencies_from_generic_parameters_rec(param.type(), refs);
@@ -974,13 +974,13 @@ std::string pretty_java_type(const typet &type)
     return "?";
 }
 
-std::string pretty_signature(const code_typet &code_type)
+std::string pretty_signature(const java_method_typet &method_type)
 {
   std::ostringstream result;
   result << '(';
 
   bool first = true;
-  for(const auto p : code_type.parameters())
+  for(const auto p : method_type.parameters())
   {
     if(p.get_this())
       continue;
diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
index cfd847eaa65..0ca7538e95a 100644
--- a/jbmc/src/java_bytecode/java_types.h
+++ b/jbmc/src/java_bytecode/java_types.h
@@ -245,6 +245,27 @@ inline bool can_cast_type<java_class_typet>(const typet &type)
 class java_method_typet : public code_typet
 {
 public:
+  using code_typet::parameterst;
+  using code_typet::parametert;
+
+  /// Constructs a new code type, i.e. method type
+  /// \param _parameters: the vector of method parameters
+  /// \param _return_type: the return type
+  java_method_typet(parameterst &&_parameters, typet &&_return_type)
+    : code_typet(std::move(_parameters), std::move(_return_type))
+  {
+    set(ID_C_java_method_type, true);
+  }
+
+  /// Constructs a new code type, i.e. method type
+  /// \param _parameters: the vector of method parameters
+  /// \param _return_type: the return type
+  java_method_typet(parameterst &&_parameters, const typet &_return_type)
+    : code_typet(std::move(_parameters), _return_type)
+  {
+    set(ID_C_java_method_type, true);
+  }
+
   const std::vector<irep_idt> throws_exceptions() const
   {
     std::vector<irep_idt> exceptions;
@@ -259,15 +280,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);
+  PRECONDITION(can_cast_type<java_method_typet>(type));
   return static_cast<java_method_typet &>(type);
 }
 
@@ -732,6 +759,6 @@ std::string gather_full_class_name(const std::string &);
 std::string pretty_java_type(const typet &);
 
 // pretty signature for methods
-std::string pretty_signature(const code_typet &);
+std::string pretty_signature(const java_method_typet &);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp
index 9e9f4f499ab..7d57ef826e6 100644
--- a/jbmc/src/java_bytecode/java_utils.cpp
+++ b/jbmc/src/java_bytecode/java_utils.cpp
@@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_utils.h"
 
 #include "java_root_class.h"
-#include "java_types.h"
 
 #include <util/invariant.h>
 #include <util/message.h>
@@ -46,7 +45,7 @@ unsigned java_local_variable_slots(const typet &t)
   return bitwidth == 64 ? 2u : 1u;
 }
 
-unsigned java_method_parameter_slots(const code_typet &t)
+unsigned java_method_parameter_slots(const java_method_typet &t)
 {
   unsigned slots=0;
 
diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h
index dea8f1bf412..e58db51594f 100644
--- a/jbmc/src/java_bytecode/java_utils.h
+++ b/jbmc/src/java_bytecode/java_utils.h
@@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
 #define CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
 
+#include "java_types.h"
+
 #include <unordered_set>
 
 #include <util/message.h>
@@ -31,7 +33,7 @@ unsigned java_local_variable_slots(const typet &t);
 
 /// Returns the the number of JVM local variables (slots) used by the JVM to
 /// pass, upon call, the arguments of a Java method whose type is \p t.
-unsigned java_method_parameter_slots(const code_typet &t);
+unsigned java_method_parameter_slots(const java_method_typet &t);
 
 const std::string java_class_to_package(const std::string &canonical_classname);
 
diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
index 4fa38a5ea03..640f68196f7 100644
--- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp
+++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
@@ -145,7 +145,7 @@ void java_simple_method_stubst::create_method_stub_at(
 void java_simple_method_stubst::create_method_stub(symbolt &symbol)
 {
   code_blockt new_instructions;
-  const code_typet &required_type = to_code_type(symbol.type);
+  const java_method_typet &required_type = to_java_method_type(symbol.type);
 
   // synthetic source location that contains the opaque function name only
   source_locationt synthesized_source_location;
diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp
index 77d09d02bc8..fb0d40e9470 100644
--- a/jbmc/unit/java-testing-utils/require_type.cpp
+++ b/jbmc/unit/java-testing-utils/require_type.cpp
@@ -75,6 +75,29 @@ require_type::require_code(const typet &type, const size_t num_params)
   return code_type;
 }
 
+/// Checks a type is a java_method_typet (i.e. a function)
+/// \param type: The type to check
+/// \return The cast version of the type method_type
+java_method_typet require_type::require_java_method(const typet &type)
+{
+  REQUIRE(can_cast_type<java_method_typet>(type));
+  return to_java_method_type(type);
+}
+
+/// Verify a given type is an java_method_typet, and that the code it represents
+/// accepts a given number of parameters
+/// \param type The type to check
+/// \param num_params check the the given java_method_typet expects this
+/// number of parameters
+/// \return The type cast to a java_method_typet
+java_method_typet
+require_type::require_java_method(const typet &type, const size_t num_params)
+{
+  java_method_typet method_type = require_java_method(type);
+  REQUIRE(method_type.parameters().size() == num_params);
+  return method_type;
+}
+
 /// Verify that a function has a parameter of a specific name.
 /// \param function_type: The type of the function
 /// \param param_name: The name of the parameter
diff --git a/jbmc/unit/java-testing-utils/require_type.h b/jbmc/unit/java-testing-utils/require_type.h
index 3e59da59e72..168a781b863 100644
--- a/jbmc/unit/java-testing-utils/require_type.h
+++ b/jbmc/unit/java-testing-utils/require_type.h
@@ -33,11 +33,14 @@ struct_typet::componentt require_component(
   const irep_idt &component_name);
 
 code_typet require_code(const typet &type);
+java_method_typet require_java_method(const typet &type);
 
 code_typet::parametert
 require_parameter(const code_typet &function_type, const irep_idt &param_name);
 
 code_typet require_code(const typet &type, const size_t num_params);
+java_method_typet
+require_java_method(const typet &type, const size_t num_params);
 
 // A mini DSL for describing an expected set of type arguments for a
 // java_generic_typet
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp
index 8583977a748..a314624c2ec 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp
@@ -33,7 +33,8 @@ void require_is_constructor(const test_datat &test_data)
     test_data.symbol_table.lookup_ref(test_data.constructor_descriptor);
   THEN("The constructor should be marked as a constructor")
   {
-    code_typet constructor_type = require_type::require_code(constructor.type);
+    java_method_typet constructor_type =
+      require_type::require_java_method(constructor.type);
     REQUIRE(constructor_type.get_is_constructor());
   }
 }
@@ -49,7 +50,8 @@ void require_is_static_initializer(const test_datat &test_data)
     test_data.symbol_table.lookup_ref(test_data.constructor_descriptor);
   THEN("The constructor should be marked as a constructor")
   {
-    code_typet constructor_type = require_type::require_code(constructor.type);
+    java_method_typet constructor_type =
+      require_type::require_java_method(constructor.type);
     REQUIRE_FALSE(constructor_type.get_is_constructor());
   }
 }
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp
index a925d8469f8..76aa4e0155e 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp
@@ -29,9 +29,13 @@ SCENARIO(
       const symbolt function_symbol =
         symbol_table.lookup_ref(method_name + ":(Ljava/lang/Object;)I");
 
-      const code_typet &function_type =
-        require_type::require_code(function_symbol.type);
-      THEN("The method should be marked as a bridge method")
+      const java_method_typet &function_type =
+        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));
       }
@@ -43,8 +47,8 @@ SCENARIO(
         const symbolt function_symbol =
           symbol_table.lookup_ref(method_name + ":(LClassWithBridgeMethod;)I");
 
-        const code_typet &function_type =
-          require_type::require_code(function_symbol.type);
+        const java_method_typet &function_type =
+          require_type::require_java_method(function_symbol.type);
         THEN("The method should be marked as a bridge method")
         {
           REQUIRE_FALSE(function_type.get_bool(ID_is_bridge_method));
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp
index 5c3fe280632..c3718d0cabb 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp
@@ -76,9 +76,9 @@ SCENARIO(
         {
           const symbolt &method_symbol =
             new_symbol_table.lookup_ref(method_name);
-          const code_typet &method_type =
-            require_type::require_code(method_symbol.type);
-          const code_typet::parametert &param =
+          const java_method_typet &method_type =
+            require_type::require_java_method(method_symbol.type);
+          const java_method_typet::parametert &param =
             require_type::require_parameter(method_type, "x");
           require_type::require_java_generic_parameter(
             param.type(), boundedinner_name + "::NUM");
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp
index 7a2845c648a..adf4c715165 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp
@@ -32,12 +32,12 @@ SCENARIO(
 
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet &func_code =
-        require_type::require_code(func_symbol.type);
+      const java_method_typet &func_code =
+        require_type::require_java_method(func_symbol.type);
 
       THEN("It has parameter x pointing to Generic")
       {
-        const code_typet::parametert &param_x =
+        const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
         require_type::require_pointer(
           param_x.type(), symbol_typet("java::Generic"));
@@ -81,11 +81,12 @@ SCENARIO(
 
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code = require_type::require_code(func_symbol.type);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type);
 
       THEN("It has parameter s pointing to Generic")
       {
-        const code_typet::parametert &param_s =
+        const java_method_typet::parametert &param_s =
           require_type::require_parameter(func_code, "s");
         require_type::require_pointer(
           param_s.type(), symbol_typet("java::Generic"));
@@ -129,11 +130,12 @@ SCENARIO(
 
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code = require_type::require_code(func_symbol.type);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type);
 
       THEN("It has parameter x pointing to Generic")
       {
-        const code_typet::parametert &param_x =
+        const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
         require_type::require_pointer(
           param_x.type(), symbol_typet("java::Generic"));
@@ -149,7 +151,7 @@ SCENARIO(
 
       THEN("It has parameter y pointing to Generic")
       {
-        const code_typet::parametert &param_y =
+        const java_method_typet::parametert &param_y =
           require_type::require_parameter(func_code, "y");
         require_type::require_pointer(
           param_y.type(), symbol_typet("java::Generic"));
@@ -193,11 +195,12 @@ SCENARIO(
 
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code = require_type::require_code(func_symbol.type);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type);
 
       THEN("It has parameter s pointing to Generic")
       {
-        const code_typet::parametert &param_s =
+        const java_method_typet::parametert &param_s =
           require_type::require_parameter(func_code, "s");
         require_type::require_pointer(
           param_s.type(), symbol_typet("java::Generic"));
@@ -213,7 +216,7 @@ SCENARIO(
 
       THEN("It has parameter b pointing to Generic")
       {
-        const code_typet::parametert &param_b =
+        const java_method_typet::parametert &param_b =
           require_type::require_parameter(func_code, "b");
         require_type::require_pointer(
           param_b.type(), symbol_typet("java::Generic"));
@@ -258,11 +261,12 @@ SCENARIO(
 
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code = require_type::require_code(func_symbol.type);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type);
 
       THEN("It has parameter inner pointing to Inner")
       {
-        const code_typet::parametert &param_inner =
+        const java_method_typet::parametert &param_inner =
           require_type::require_parameter(func_code, "inner");
         require_type::require_pointer(
           param_inner.type(), symbol_typet(class_prefix + "$Inner"));
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp
index 47de0300e5b..ca763c5e463 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp
@@ -316,8 +316,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs are of correct type")
     {
@@ -345,8 +345,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 3);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 3);
 
     THEN("The inputs are of correct type")
     {
@@ -381,8 +381,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs are of correct type")
     {
@@ -412,8 +412,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs are of correct type")
     {
@@ -442,8 +442,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs are of correct type")
     {
@@ -476,8 +476,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs are of correct type")
     {
@@ -508,8 +508,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs are of correct type")
     {
@@ -544,8 +544,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs are of correct type")
     {
@@ -576,8 +576,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs are of the correct type")
     {
@@ -609,8 +609,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs are of the correct type")
     {
@@ -642,8 +642,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs should be of the correct type")
     {
@@ -672,8 +672,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type should be correct")
     {
@@ -699,8 +699,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type should be correct")
     {
@@ -729,8 +729,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type should be correct")
     {
@@ -758,8 +758,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type should be correct")
     {
@@ -790,8 +790,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type should be correct")
     {
@@ -820,8 +820,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type should be correct")
     {
@@ -854,8 +854,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type should be correct")
     {
@@ -885,8 +885,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type should be correct")
     {
@@ -917,8 +917,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type should be correct")
     {
@@ -949,8 +949,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type should be correct")
     {
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp
index 41faa1bae19..b7dbdcdb1b0 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp
@@ -32,11 +32,11 @@ SCENARIO(
 
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 1);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 1);
       THEN("It contains parameter x pointing to Generic")
       {
-        const code_typet::parametert &param_x =
+        const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
         require_type::require_pointer(
           param_x.type(), symbol_typet("java::Generic"));
@@ -59,11 +59,11 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 1);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 1);
       THEN("It contains parameter x pointing to Generic")
       {
-        const code_typet::parametert &param_x =
+        const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
         require_type::require_pointer(
           param_x.type(), symbol_typet("java::Generic"));
@@ -86,11 +86,11 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 1);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 1);
       THEN("It contains parameter x pointing to Generic")
       {
-        const code_typet::parametert &param_x =
+        const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
         require_type::require_pointer(
           param_x.type(), symbol_typet("java::Generic"));
@@ -113,11 +113,11 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 1);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 1);
       THEN("It contains parameter x pointing to java.lang.Number")
       {
-        const code_typet::parametert &param_x =
+        const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
         require_type::require_pointer(
           param_x.type(), symbol_typet("java::java.lang.Number"));
@@ -140,11 +140,11 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 1);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 1);
       THEN("It contains parameter x pointing to Generic")
       {
-        const code_typet::parametert &param_x =
+        const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
         require_type::require_pointer(
           param_x.type(), symbol_typet("java::Generic"));
@@ -167,11 +167,11 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 1);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 1);
       THEN("It contains parameter x pointing to Generic")
       {
-        const code_typet::parametert &param_x =
+        const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
         require_type::require_pointer(
           param_x.type(), symbol_typet("java::Generic"));
@@ -194,12 +194,12 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 2);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 2);
 
       THEN("It contains parameter t pointing to Generic")
       {
-        const code_typet::parametert &param_t =
+        const java_method_typet::parametert &param_t =
           require_type::require_parameter(func_code, "t");
         require_type::require_pointer(
           param_t.type(), symbol_typet("java::Generic"));
@@ -209,7 +209,7 @@ SCENARIO(
       }
       THEN("It contains parameter u pointing to Generic")
       {
-        const code_typet::parametert &param_u =
+        const java_method_typet::parametert &param_u =
           require_type::require_parameter(func_code, "u");
         require_type::require_pointer(
           param_u.type(), symbol_typet("java::Generic"));
@@ -232,12 +232,12 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 2);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 2);
 
       THEN("It contains parameter t pointing to Generic")
       {
-        const code_typet::parametert &param_t =
+        const java_method_typet::parametert &param_t =
           require_type::require_parameter(func_code, "t");
         require_type::require_pointer(
           param_t.type(), symbol_typet("java::Generic"));
@@ -247,7 +247,7 @@ SCENARIO(
       }
       THEN("It contains parameter u pointing to Generic")
       {
-        const code_typet::parametert &param_u =
+        const java_method_typet::parametert &param_u =
           require_type::require_parameter(func_code, "u");
         require_type::require_pointer(
           param_u.type(), symbol_typet("java::Generic"));
@@ -271,8 +271,8 @@ SCENARIO(
 
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 0);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 0);
       THEN("It has return type pointing to Generic")
       {
         require_type::require_pointer(
@@ -297,8 +297,8 @@ SCENARIO(
 
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 0);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 0);
       THEN("It has return type pointing to java.lang.Object")
       {
         require_type::require_pointer(
@@ -322,7 +322,7 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code = to_code_type(func_symbol.type);
+      const java_method_typet func_code = to_java_method_type(func_symbol.type);
       THEN("It has return type pointing to Generic")
       {
         require_type::require_pointer(
@@ -346,8 +346,8 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 0);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 0);
       THEN("It has return type pointing to Generic")
       {
         require_type::require_pointer(
@@ -371,8 +371,8 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 0);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 0);
       THEN("It has return type pointing to Generic")
       {
         require_type::require_pointer(
@@ -396,8 +396,8 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 0);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 0);
       THEN("It has return type pointing to Generic")
       {
         require_type::require_pointer(
@@ -422,12 +422,12 @@ SCENARIO(
 
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 1);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 1);
 
       THEN("It contains parameter x pointing to Generic")
       {
-        const code_typet::parametert &param_x =
+        const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
         require_type::require_pointer(
           param_x.type(), symbol_typet("java::Generic"));
@@ -459,12 +459,12 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 1);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 1);
 
       THEN("It contains parameter x pointing to Generic")
       {
-        const code_typet::parametert &param_x =
+        const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
         require_type::require_pointer(
           param_x.type(), symbol_typet("java::Generic"));
@@ -496,12 +496,12 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 1);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 1);
 
       THEN("It contains parameter x pointing to Generic")
       {
-        const code_typet::parametert &param_x =
+        const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
         require_type::require_pointer(
           param_x.type(), symbol_typet("java::Generic"));
@@ -533,12 +533,12 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 1);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 1);
 
       THEN("It contains parameter x pointing to Generic")
       {
-        const code_typet::parametert &param_x =
+        const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
         require_type::require_pointer(
           param_x.type(), symbol_typet("java::Generic"));
@@ -571,12 +571,12 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 1);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 1);
 
       THEN("It contains parameter x pointing to Generic")
       {
-        const code_typet::parametert &param_x =
+        const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
         require_type::require_pointer(
           param_x.type(), symbol_typet("java::Generic"));
@@ -608,12 +608,12 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 1);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 1);
 
       THEN("It contains parameter u pointing to Generic")
       {
-        const code_typet::parametert &param_u =
+        const java_method_typet::parametert &param_u =
           require_type::require_parameter(func_code, "u");
         require_type::require_pointer(
           param_u.type(), symbol_typet("java::Generic"));
@@ -645,12 +645,12 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 1);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 1);
 
       THEN("It contains parameter u pointing to Generic")
       {
-        const code_typet::parametert &param_u =
+        const java_method_typet::parametert &param_u =
           require_type::require_parameter(func_code, "u");
         require_type::require_pointer(
           param_u.type(), symbol_typet("java::Generic"));
@@ -682,12 +682,12 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 2);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 2);
 
       THEN("It contains parameter u pointing to Generic")
       {
-        const code_typet::parametert &param_u =
+        const java_method_typet::parametert &param_u =
           require_type::require_parameter(func_code, "u");
         require_type::require_pointer(
           param_u.type(), symbol_typet("java::Generic"));
@@ -698,7 +698,7 @@ SCENARIO(
 
       THEN("It contains parameter v pointing to Generic")
       {
-        const code_typet::parametert &param_v =
+        const java_method_typet::parametert &param_v =
           require_type::require_parameter(func_code, "v");
         require_type::require_pointer(
           param_v.type(), symbol_typet("java::Generic"));
@@ -730,12 +730,12 @@ SCENARIO(
       REQUIRE(new_symbol_table.has_symbol(process_func_name));
       const symbolt func_symbol =
         new_symbol_table.lookup_ref(process_func_name);
-      const code_typet func_code =
-        require_type::require_code(func_symbol.type, 2);
+      const java_method_typet func_code =
+        require_type::require_java_method(func_symbol.type, 2);
 
       THEN("It contains parameter u pointing to Generic")
       {
-        const code_typet::parametert &param_u =
+        const java_method_typet::parametert &param_u =
           require_type::require_parameter(func_code, "u");
         require_type::require_pointer(
           param_u.type(), symbol_typet("java::Generic"));
@@ -746,7 +746,7 @@ SCENARIO(
 
       THEN("It contains parameter v pointing to Generic")
       {
-        const code_typet::parametert &param_v =
+        const java_method_typet::parametert &param_v =
           require_type::require_parameter(func_code, "v");
         require_type::require_pointer(
           param_v.type(), symbol_typet("java::Generic"));
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp
index e3e5cf657ce..d7b03574414 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp
@@ -417,8 +417,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs are of correct type")
     {
@@ -455,8 +455,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs are of oorrect type")
     {
@@ -493,8 +493,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs are of correct type")
     {
@@ -538,8 +538,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs are of correct type")
     {
@@ -583,8 +583,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs are of correct type")
     {
@@ -624,8 +624,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs have correct type")
     {
@@ -665,8 +665,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs have correct type")
     {
@@ -706,8 +706,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs have correct type")
     {
@@ -751,8 +751,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs have correct type")
     {
@@ -796,8 +796,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs have correct type")
     {
@@ -841,8 +841,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs have correct type")
     {
@@ -882,8 +882,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs have correct type")
     {
@@ -929,8 +929,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 2);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 2);
 
     THEN("The inputs have correct type")
     {
@@ -976,8 +976,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type is correct")
     {
@@ -1012,8 +1012,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type is correct")
     {
@@ -1048,8 +1048,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type is correct")
     {
@@ -1090,8 +1090,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type is correct")
     {
@@ -1132,8 +1132,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type is correct")
     {
@@ -1171,8 +1171,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type is correct")
     {
@@ -1210,8 +1210,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type is correct")
     {
@@ -1249,8 +1249,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type is correct")
     {
@@ -1292,8 +1292,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type is correct")
     {
@@ -1335,8 +1335,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type is correct")
     {
@@ -1378,8 +1378,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type is correct")
     {
@@ -1417,8 +1417,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type is correct")
     {
@@ -1462,8 +1462,8 @@ SCENARIO(
     const symbolt &function_symbol =
       new_symbol_table.lookup_ref(process_func_name);
 
-    const code_typet &function_call =
-      require_type::require_code(function_symbol.type, 1);
+    const java_method_typet &function_call =
+      require_type::require_java_method(function_symbol.type, 1);
 
     THEN("The return type is correct")
     {
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp
index 7cbdd2f55ac..fdae9d90a82 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp
@@ -43,16 +43,16 @@ SCENARIO(
       inner_prefix + func_name + func_descriptor;
     REQUIRE(new_symbol_table.has_symbol(process_func_name));
 
-    const code_typet func_code =
-      to_code_type(new_symbol_table.lookup_ref(process_func_name).type);
+    const java_method_typet func_code =
+      to_java_method_type(new_symbol_table.lookup_ref(process_func_name).type);
     REQUIRE(func_code.parameters().size() == 3);
 
     // TODO: for now, the parameters are not generic because we fall back to
     // descriptor due to mismatch; enable tests when fixed - issue TG-1309
-    // code_typet::parametert param_parent=
+    // java_method_typet::parametert param_parent=
     //  require_type::require_parameter(func_code,"arg1a");
     // REQUIRE(is_java_generic_type(param_parent.type()));
-    // code_typet::parametert param_t=
+    // java_method_typet::parametert param_t=
     //  require_type::require_parameter(func_code,"t");
     // REQUIRE(is_java_generic_type(param_t.type()));
   }
@@ -78,16 +78,16 @@ SCENARIO(
       inner_enum_prefix + func_name + func_descriptor;
     REQUIRE(new_symbol_table.has_symbol(process_func_name));
 
-    const code_typet func_code =
-      to_code_type(new_symbol_table.lookup_ref(process_func_name).type);
+    const java_method_typet func_code =
+      to_java_method_type(new_symbol_table.lookup_ref(process_func_name).type);
     REQUIRE(func_code.parameters().size() == 3);
 
     // TODO: for now, the parameters are not generic because we fall back to
     // descriptor due to mismatch; enable tests when fixed - issue TG-1309
-    // code_typet::parametert param_parent=
+    // java_method_typet::parametert param_parent=
     //  require_type::require_parameter(func_code,"arg1a");
     // REQUIRE(is_java_generic_type(param_parent.type()));
-    // code_typet::parametert param_t=
+    // java_method_typet::parametert param_t=
     //  require_type::require_parameter(func_code,"arg2i");
     // REQUIRE(is_java_generic_type(param_t.type()));
   }
diff --git a/jbmc/unit/java_bytecode/load_method_by_regex.cpp b/jbmc/unit/java_bytecode/load_method_by_regex.cpp
index 5b754996728..8b79894a1ca 100644
--- a/jbmc/unit/java_bytecode/load_method_by_regex.cpp
+++ b/jbmc/unit/java_bytecode/load_method_by_regex.cpp
@@ -92,7 +92,7 @@ static symbolt create_method_symbol(const std::string &method_name)
 {
   symbolt new_symbol;
   new_symbol.name = method_name;
-  new_symbol.type = code_typet{{}, nil_typet{}};
+  new_symbol.type = java_method_typet{{}, nil_typet{}};
   return new_symbol;
 }
 
diff --git a/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp b/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp
index 1e7b9461e26..64856fddb96 100644
--- a/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp
+++ b/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp
@@ -58,11 +58,11 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
     const symbol_exprt lhs("lhs", unsignedbv_typet(32));
     const symbol_exprt lhs2("lhs2", unsignedbv_typet(32));
     const symbol_exprt lhs3("lhs3", unsignedbv_typet(32));
-    const code_typet fun_type(
-      {code_typet::parametert(length_type()),
-       code_typet::parametert(pointer_type(java_char_type())),
-       code_typet::parametert(string_type),
-       code_typet::parametert(string_type)},
+    const java_method_typet fun_type(
+      {java_method_typet::parametert(length_type()),
+       java_method_typet::parametert(pointer_type(java_char_type())),
+       java_method_typet::parametert(string_type),
+       java_method_typet::parametert(string_type)},
       unsignedbv_typet(32));
 
     // fun1 is s3 = s1.concat(s2)
diff --git a/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp b/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp
index e7b6eb22478..443e9126a5f 100644
--- a/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp
+++ b/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp
@@ -64,7 +64,10 @@ SCENARIO("string_identifiers_resolution_from_equations",
 
     WHEN("There is a function call")
     {
-      symbol_exprt fun_sym("f", code_typet());
+      java_method_typet::parameterst parameters;
+      typet return_type;
+      symbol_exprt fun_sym(
+        "f", java_method_typet(std::move(parameters), return_type));
       function_application_exprt fun(fun_sym, bool_typet());
       fun.operands().push_back(c);
       symbol_exprt bool_sym("bool_b", bool_typet());
diff --git a/jbmc/unit/util/parameter_indices.cpp b/jbmc/unit/util/parameter_indices.cpp
index f29f76f1c27..df41d773c77 100644
--- a/jbmc/unit/util/parameter_indices.cpp
+++ b/jbmc/unit/util/parameter_indices.cpp
@@ -6,15 +6,16 @@
 
 \*******************************************************************/
 
+#include <java_bytecode/java_types.h>
+
 #include <testing-utils/catch.hpp>
 #include <java-testing-utils/load_java_class.h>
-#include <util/std_types.h>
 
 void check_consistency(const symbolt &symbol)
 {
-  const auto &code_type = to_code_type(symbol.type);
-  auto parameter_ids = code_type.parameter_identifiers();
-  auto parameter_indices = code_type.parameter_indices();
+  const auto &method_type = to_java_method_type(symbol.type);
+  auto parameter_ids = method_type.parameter_identifiers();
+  auto parameter_indices = method_type.parameter_indices();
 
   REQUIRE(parameter_ids.size() == parameter_indices.size());
   for(std::size_t i = 0; i < parameter_ids.size(); ++i)
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index d0066054482..7687299a1fb 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -697,6 +697,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