Add documentation to memory snapshot harness

This may need modification after #4150 is merged.

Author: Petr Bauch

src/goto-harness/memory_snapshot_harness_generator.h

@@ -32,6 +32,8 @@ Author: Daniel Poetzl
   "--initial-location <func[:<n>]>\n"                                          \
   "                              use given function and location number as "   \
   "entry\n                              point\n"                               \
+  "--havoc-variables vars        initialise variables from vars to\n"          \
+  "                              non-deterministic values"                     \
   // MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP
 // clang-format on
 
@@ -47,30 +49,93 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
   {
   }
 
+  /// 1. load memory table from the snapshot
+  /// 2. add initial section to the initial location
+  /// 3. assign global variables their snapshot values (via the harness
+  ///    function)
+  /// 4. insert call of the initial location (with nondet values) into the
+  ///    harness function
+  /// 5. build symbol for the harness functions
+  /// 6. insert harness function into \p goto_model
+  /// \param goto_model: goto model to be modified
+  /// \param harness_function_name: name of the resulting harness function
   void generate(goto_modelt &goto_model, const irep_idt &harness_function_name)
     override;
 
 protected:
+  /// Collect the memory-snapshot specific cmdline options (one at a time)
+  /// \param option: memory-snapshot | initial-location | havoc-variables
+  /// \param values: list of arguments related to a given option
   void handle_option(
     const std::string &option,
     const std::list<std::string> &values) override;
 
+  /// Check that user options make sense:
+  /// On their own, e.g. location number cannot be specified without a function.
+  /// In relation to the input program, e.g. function name must be known via
+  ///   the symbol table.
   void validate_options() override;
 
+  /// Parse the snapshot JSON file and initialise the symbol table
+  /// \param file: the snapshot JSON file
+  /// \param snapshot: the resulting symbol table build from the snapshot
   void
   get_memory_snapshot(const std::string &file, symbol_tablet &snapshot) const;
 
+  /// Turn this:
+  /// --------------------------------------------------------------------------
+  ///    int foo() {
+  ///      ..first_part..
+  /// i:   //location_number=i
+  ///      ..second_part..
+  ///    }
+  /// --------------------------------------------------------------------------
+
+  /// Into this:
+  /// --------------------------------------------------------------------------
+  ///   func_init_done;
+  ///   __CPROVER_initialize() {
+  ///     ...
+  ///     func_init_done = false;
+  ///   }
+  ///   int foo() {
+  ///     if (func_init_done) goto 1;
+  ///     func_init_done = true;
+  ///     goto i;
+  /// 1:  ;
+  ///     ..first_part..
+  /// i:  //location_number=i
+  ///     ..second_part..
+  ///   }
+  /// --------------------------------------------------------------------------
+  /// \param goto_model: Model where the modification takes place
   void add_init_section(goto_modelt &goto_model) const;
 
+  /// For each global symbol in the \p snapshot symbol table either:
+  /// 1) add \ref code_assignt assigning a value from the \snapshot to the
+  ///    symbol
+  /// 2) recursively initialise the symbol to a non-deterministic value of the
+  ///    right type
+  /// \param snapshot: snapshot to load the symbols and their values from
+  /// \param goto_model: model to initialise the havoc-ing
+  /// \param code: block of code where the assignments are added
   void add_assignments_to_globals(
     const symbol_tablet &snapshot,
     goto_modelt &goto_model,
     code_blockt &code) const;
 
+  /// Create as many non-deterministic arguments as there are arguments of the
+  /// \p called_function_symbol and add a function call with those arguments
+  /// \param called_function_symbol: the function to be called
+  /// \param code: the block of code where the function call is added
   void add_call_with_nondet_arguments(
     const symbolt &called_function_symbol,
     code_blockt &code) const;
 
+  /// Insert the \p function into the symbol table (and the goto functions map)
+  /// of the \p goto_model
+  /// \param goto_model: goto model where the insertion is to take place
+  /// \param function: symbol of the function to be inserted
   void insert_function(goto_modelt &goto_model, const symbolt &function) const;
 
   std::string memory_snapshot;