Document collect_allocations and invalidate

Author: petr-bauch

src/analyses/goto_check.cpp

@@ -79,6 +79,11 @@ class goto_checkt
     const irep_idt &function_identifier,
     goto_functiont &goto_function);
 
+  /// Fill the list of allocations \ref allocationst with <address, size> for
+  ///   every allocation instruction. Also check that each allocation is
+  ///   well-formed.
+  /// \param goto_functions: goto functions from which the allocations are to be
+  ///   collected
   void collect_allocations(const goto_functionst &goto_functions);
 
 protected:
@@ -194,6 +199,10 @@ class goto_checkt
   typedef std::set<exprt> assertionst;
   assertionst assertions;
 
+  /// Remove all assertions containing they symbol in \p lhs as well as all
+  ///   assertions containing dereference.
+  /// \param lhs: the left-hand-side expression whose symbol should be
+  ///   invalidated
   void invalidate(const exprt &lhs);
 
   bool enable_bounds_check;