Add two-param code_typet constructors and deprecate the default one

Author: peterschrammel

src/util/std_types.h

@@ -758,6 +758,31 @@ inline c_enum_tag_typet &to_c_enum_tag_type(typet &type)
 class code_typet:public typet
 {
 public:
+  class parametert;
+  typedef std::vector<parametert> parameterst;
+
+  /// Constructs a new code type, i.e. function type
+  /// \param _parameters: the vector of function parameters
+  /// \param _return_type: the return type
+  code_typet(parameterst &&_parameters, typet &&_return_type)
+   : typet(ID_code)
+  {
+    parameters().swap(_parameters);
+    return_type().swap(_return_type);
+  }
+
+  /// Constructs a new code type, i.e. function type
+  /// \param _parameters: the vector of function parameters
+  /// \param _return_type: the return type
+  code_typet(parameterst &&_parameters, const typet &_return_type)
+   : typet(ID_code)
+  {
+    parameters().swap(_parameters);
+    return_type() = _return_type;
+  }
+
+  /// \deprecated
+  DEPRECATED("Use the two argument constructor instead")
   code_typet():typet(ID_code)
   {
     // make sure these properties are always there to avoid problems
@@ -862,8 +887,6 @@ class code_typet:public typet
     add(ID_parameters).remove(ID_ellipsis);
   }
 
-  typedef std::vector<parametert> parameterst;
-
   const typet &return_type() const
   {
     return find_type(ID_return_type);