Move documentation of allocate_dynamic_object to header

Following the coding standard.

Author: antlechner

src/util/allocate_objects.cpp

@@ -121,24 +121,6 @@ symbol_exprt allocate_objectst::allocate_automatic_local_object(
   return aux_symbol.symbol_expr();
 }
 
-/// Generates code for allocating a dynamic object. A new variable with basename
-/// prefix `alloc_site` is introduced to which the allocated memory is assigned.
-/// Then, the variable is assigned to `target_expr`. For example, with
-/// `target_expr` being `*p` the following code is generated:
-///
-/// `alloc_site$1 = ALLOCATE(object_size, FALSE);`
-/// `*p = alloc_site$1;`
-///
-/// The function returns a dereference expressiont that dereferences the
-/// allocation site variable (e.g., `*alloc_site$1`) and which can be used to
-/// initialize the allocated memory.
-///
-/// \param output_code: Code block to which the necessary code is added
-/// \param target_expr: A pointer to the allocated memory will be assigned to
-///   this (lvalue) expression
-/// \param allocate_type: Type of the object allocated
-/// \return A dereference_exprt that dereferences the pointer to the allocated
-///   memory, or an empty expression when `allocate_type` is void
 exprt allocate_objectst::allocate_dynamic_object(
   code_blockt &output_code,
   const exprt &target_expr,

src/util/allocate_objects.h

@@ -62,6 +62,25 @@ class allocate_objectst
     const typet &allocate_type,
     const irep_idt &basename_prefix = "tmp");
 
+  /// Generates code for allocating a dynamic object. A new variable with
+  /// basename prefix `alloc_site` is introduced to which the allocated memory
+  /// is assigned.
+  /// Then, the variable is assigned to `target_expr`. For example, with
+  /// `target_expr` being `*p` the following code is generated:
+  ///
+  /// `alloc_site$1 = ALLOCATE(object_size, FALSE);`
+  /// `*p = alloc_site$1;`
+  ///
+  /// The function returns a dereference expressiont that dereferences the
+  /// allocation site variable (e.g., `*alloc_site$1`) and which can be used to
+  /// initialize the allocated memory.
+  ///
+  /// \param output_code: Code block to which the necessary code is added
+  /// \param target_expr: A pointer to the allocated memory will be assigned to
+  ///   this (lvalue) expression
+  /// \param allocate_type: Type of the object allocated
+  /// \return A dereference_exprt that dereferences the pointer to the allocated
+  ///   memory, or an empty expression when `allocate_type` is void
   exprt allocate_dynamic_object(
     code_blockt &output_code,
     const exprt &target_expr,