Document symex_function_call functions

This documents (mostly in goto_symex.h) functions that are defined in symex_function_call.cpp.

Author: romainbrenguier

src/goto-symex/goto_symex.h

@@ -271,25 +271,41 @@ class goto_symext
 
   virtual void loop_bound_exceeded(statet &, const exprt &guard);
 
-  // function calls
+  /// Assuming \p state is currently pointing on a return instruction, assign
+  /// the value in that return to the top frame's \p return_value field.
   void return_assignment(statet &);
 
   virtual void no_body(const irep_idt &)
   {
   }
 
+  /// Symbolic execution of a function call.
+  /// Only functions that are symbols are supported, see
+  /// \link goto_symext::symex_function_call_symbol \endlink
   virtual void symex_function_call(
     const get_goto_functiont &,
     statet &,
     const code_function_callt &);
 
   virtual void symex_end_of_function(statet &);
 
+  /// Symbolic execution of a call to a function call.
+  /// For functions \c CBMC_trace and functions starting with \c __CPROVER_fkt
+  /// see \link goto_symext::symex_trace \endlink and
+  /// \link goto_symext::symex_fkt \endlink.
+  /// For non-special functions see
+  /// \link goto_symext::symex_function_call_code \endlink
   virtual void symex_function_call_symbol(
     const get_goto_functiont &,
     statet &,
     const code_function_callt &);
 
+  /// Symbolic execution of a function call by inlining.
+  /// Records the call in \p target by appending a function call step and:
+  ///   - if the body is available create a new frame, assigns the parameters,
+  ///    and proceed to executing the code of the function.
+  ///   - otherwise assign a nondetministic value to the left-hand-side of the
+  ///     call when there is one
   virtual void symex_function_call_code(
     const get_goto_functiont &,
     statet &,
@@ -300,6 +316,12 @@ class goto_symext
     unsigned thread_nr,
     unsigned unwind);
 
+  /// Iterates over \p arguments and assign them to the parameters, which are
+  /// symbols whose name and type are deduce from the type of \p goto_function.
+  /// \param function_identifier: name of the function
+  /// \param goto_function: function whose parameters we want to assign
+  /// \param [out] state: state of the goto program
+  /// \param arguments: arguments that are passed to the function
   void parameter_assignments(
     const irep_idt &function_identifier,
     const goto_functionst::goto_functiont &,

src/goto-symex/symex_function_call.cpp

@@ -226,7 +226,6 @@ void goto_symext::symex_function_call_symbol(
     symex_function_call_code(get_goto_function, state, code);
 }
 
-/// do function call by inlining
 void goto_symext::symex_function_call_code(
   const get_goto_functiont &get_goto_function,
   statet &state,