More documentation of functions in shadow_memory_util.h

Author: NlightNFotis

src/goto-symex/shadow_memory_util.cpp

@@ -348,20 +348,19 @@ static void or_elements(
   }
 }
 
-/// Translate a list of values into an or expression. Used here in the implementation
-/// of aggregation of boolean-typed fields.
-/// \param field_type The type of the values of the or expression (expected to be
-///    the same).
+/// Translate a list of values into an or expression. Used here in the
+/// implementation of aggregation of boolean-typed fields.
+/// \param field_type The type of the values of the or expression (expected to
+///    be the same).
 /// \param values A list (std::vector) of values collected previously, passed
-///    through immediatelly to the constructed expression as operands.
+///    through immediately to the constructed expression as operands.
 /// \return A newly constructed or_exprt over the possible values given.
 static exprt or_values(const exprt::operandst &values, const typet &field_type)
 {
   if(values.size() == 1)
   {
     return values[0];
   }
-  // TODO: FOTIS: Just `or_exprt`?
   return multi_ary_exprt(ID_bitor, values, field_type);
 }
 

src/goto-symex/shadow_memory_util.h

@@ -64,7 +64,9 @@ void log_value_set(
   const messaget &log,
   const std::vector<exprt> &value_set);
 
-/// Log a match between a value in the value set of a given expression, and
+/// Log a match between an address and a value the value set. This version of
+/// the function reports more details, including the base address, the pointer
+/// and the shadow value.
 void log_value_set_match(
   const namespacet &ns,
   const messaget &log,
@@ -74,7 +76,7 @@ void log_value_set_match(
   const exprt &expr,
   const value_set_dereferencet::valuet &shadow_dereference);
 
-// TODO: doxygen
+/// Logs a successful match between an address and a value within the value set.
 void log_value_set_match(
   const namespacet &ns,
   const messaget &log,
@@ -87,17 +89,27 @@ void log_try_shadow_address(
   const messaget &log,
   const shadow_memory_statet::shadowed_addresst &shadowed_address);
 
-// TODO: doxygen
+/// Generic logging function that will log depending on the configured
+/// verbosity. Will log a specific message given to it, along with an expression
+/// passed along to it.
 void log_cond(
   const namespacet &ns,
   const messaget &log,
   const char *cond_text,
   const exprt &cond);
 
-// TODO: doxygen
+/// Replace an invalid object by a null pointer. Works recursively on the
+/// operands (child nodes) of the expression, as well.
+/// \param expr The (root) expression where substitution will happen.
 void replace_invalid_object_by_null(exprt &expr);
 
-// TODO: doxygen
+/// Retrieve the expression that a field was initialised with within a given
+/// symex state.
+/// \param field_name The field whose initialisation expression we want to
+///   retrieve.
+/// \param state The goto symex state within which we want to search for the
+///   expression.
+/// \returns The expression the field was initialised with.
 const exprt &
 get_field_init_expr(const irep_idt &field_name, const goto_symex_statet &state);
 
@@ -155,7 +167,7 @@ exprt compute_max_over_cells(
 /// \param conds_values Contains pairs <e1, e2>, where `e1` is going to be
 ///    used as an antecedent for an if_expr, and `e2` is going to be used
 ///    as the consequent.
-/// \returns An if_exprt of the form `if e1 then e2 else <if e3 then e4 else ...`
+/// \returns An if_exprt of the form `if e1 then e2 else if e3 then e4 else ...`
 exprt build_if_else_expr(
   const std::vector<std::pair<exprt, exprt>> &conds_values);
 
@@ -170,9 +182,9 @@ bool set_field_check_null(
 /// Get shadow memory values for a given expression within a specified value
 /// set.
 /// \returns if potential values are present for that object inside the value
-///    set, then we get back an `if e1 then e2 else (if e3 else e4...` expression,
-///    where `e1`, `e3`, ... are guards (conditions) and `e2`, `e4`, etc are
-///    the possible values of the object within the value set.
+///    set, then we get back an `if e1 then e2 else (if e3 else e4...`
+///    expression, where `e1`, `e3`, ... are guards (conditions) and `e2`, `e4`,
+///    etc are the possible values of the object within the value set.
 optionalt<exprt> get_shadow_memory(
   const exprt &expr,
   const std::vector<exprt> &value_set,