Document nondet-static functions

Author: svorenova

src/goto-instrument/nondet_static.cpp

@@ -49,7 +49,13 @@ bool is_nondet_initializable_static(
          !is_constant_or_has_constant_components(ns.lookup(id).type, ns);
 }
 
-
+/// Nondeterministically initializes certain global scope variables in a
+/// goto-function. Iterates over instructions in the specified function
+/// and replaces all values assigned to nondet-initializable static variables
+/// by nondeterministic values.
+/// \param ns Namespace for resolving type information.
+/// \param goto_functions Existing goto-functions to be updated.
+/// \param fct_name Name of the goto-function to be updated.
 void nondet_static(
   const namespacet &ns,
   goto_functionst &goto_functions,
@@ -93,6 +99,10 @@ void nondet_static(
   }
 }
 
+/// Nondeterministically initializes certain global scope variables in
+/// CPROVER_initialize function.
+/// \param ns Namespace for resolving type information.
+/// \param goto_functions Existing goto-functions to be updated.
 void nondet_static(
   const namespacet &ns,
   goto_functionst &goto_functions)
@@ -103,6 +113,9 @@ void nondet_static(
   goto_functions.update();
 }
 
+/// Main entry point of the module. Nondeterministically initializes certain
+/// global scope variables.
+/// \param [out] goto_model Existing goto-model to be updated.
 void nondet_static(goto_modelt &goto_model)
 {
   const namespacet ns(goto_model.symbol_table);