Merge pull request #4076 from romainbrenguier/doc/symex-trace2

Document build_goto_trace [DOC-136]

Author: romainbrenguier

src/goto-symex/build_goto_trace.cpp

@@ -25,7 +25,7 @@ Author: Daniel Kroening
 
 #include "partial_order_concurrency.h"
 
-exprt build_full_lhs_rec(
+static exprt build_full_lhs_rec(
   const prop_convt &prop_conv,
   const namespacet &ns,
   const exprt &src_original, // original identifiers
@@ -104,7 +104,7 @@ exprt build_full_lhs_rec(
 
 /// set internal field for variable assignment related to dynamic_object[0-9]
 /// and dynamic_[0-9]_array.
-void set_internal_dynamic_object(
+static void set_internal_dynamic_object(
   const exprt &expr,
   goto_trace_stept &goto_trace_step,
   const namespacet &ns)
@@ -132,7 +132,7 @@ void set_internal_dynamic_object(
 
 /// set internal for variables assignments related to dynamic_object and CPROVER
 /// internal functions (e.g., __CPROVER_initialize)
-void update_internal_field(
+static void update_internal_field(
   const symex_target_equationt::SSA_stept &SSA_step,
   goto_trace_stept &goto_trace_step,
   const namespacet &ns)

src/goto-symex/build_goto_trace.h

@@ -17,14 +17,25 @@ Date: July 2005
 #include "symex_target_equation.h"
 #include "goto_symex_state.h"
 
-// builds a trace that stops at first failing assertion
+/// Build a trace by going through the steps of \p target and stopping at the
+/// first failing assertion
+/// \param target: SSA form of the program
+/// \param prop_conv: solver from which to get valuations
+/// \param ns: namespace
+/// \param [out] goto_trace: trace to which the steps of the trace get appended
 void build_goto_trace(
   const symex_target_equationt &target,
   const prop_convt &prop_conv,
   const namespacet &ns,
   goto_tracet &goto_trace);
 
-// builds a trace that stops after the given step
+/// Build a trace by going through the steps of \p target and stopping after
+/// the given step
+/// \param target: SSA form of the program
+/// \param last_step_to_keep: iterator pointing to the last step to keep
+/// \param prop_conv: solver from which to get valuations
+/// \param ns: namespace
+/// \param [out] goto_trace: trace to which the steps of the trace get appended
 void build_goto_trace(
   const symex_target_equationt &target,
   symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
@@ -36,7 +47,14 @@ typedef std::function<
   bool(symex_target_equationt::SSA_stepst::const_iterator, const prop_convt &)>
   ssa_step_predicatet;
 
-// builds a trace that stops after the step matching a given condition
+/// Build a trace by going through the steps of \p target and stopping after
+/// the step matching a given condition
+/// \param target: SSA form of the program
+/// \param stop_after_predicate: function with an SSA step iterator and solver
+///   as argument, which should return true for the last step to keep
+/// \param prop_conv: solver from which to get valuations
+/// \param ns: namespace
+/// \param [out] goto_trace: trace to which the steps of the trace get appended
 void build_goto_trace(
   const symex_target_equationt &target,
   ssa_step_predicatet stop_after_predicate,