Add documentation

Add documentation for doxygen and also improve type clarity

Author: TGWDB

src/goto-programs/builtin_functions.cpp

@@ -624,7 +624,7 @@ void goto_convertt::do_enum_is_in_range(
   const c_enum_typet &c_enum_type = ns.follow_tag(*enum_type);
   const c_enum_typet::memberst enum_values = c_enum_type.members();
 
-  std::vector<exprt> disjuncts;
+  exprt::operandst disjuncts;
   for(const auto &enum_value : enum_values)
   {
     constant_exprt val{enum_value.get_value(), *enum_type};

src/goto-programs/goto_convert_class.h

@@ -588,12 +588,27 @@ class goto_convertt:public messaget
   bool get_string_constant(const exprt &expr, irep_idt &);
   exprt get_constant(const exprt &expr);
 
-  // some built-in functions
+  /// \brief Converts calls to the built in `enum_is_in_range` function to a
+  ///    test that the given enum value is in the valid range of values for that
+  ///    enum type.
+  ///
+  /// Note that the check for the range of values is done by creating a
+  /// disjunction comparing the expression with each possible valid value.
+  /// \param lhs The destination for the generated assignment.
+  /// \param function The `enum_is_in_range` symbol of the source function call.
+  /// \param arguments A collection of arguments, which is expected to contain a
+  ///    single argument which is an expression that resolves to a value of
+  ///    enum type. The arguments are expected to have been prevalidated by the
+  ///    typechecking process.
+  /// \param dest The goto program into which the generated assignment is
+  ///    copied.
   void do_enum_is_in_range(
     const exprt &lhs,
     const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
+
+  // some built-in functions
   void do_atomic_begin(
     const exprt &lhs,
     const symbol_exprt &function,