Merge pull request #3430 from johnnonweiler/doc/reduce-doxygen-warnings-18

Fix Doxygen warnings in goto-instrument/wmm folder

Author: Daniel Kroening

scripts/expected_doxygen_warnings.txt

@@ -19,21 +19,3 @@
 /cbmc/doc/architectural/howto.md:260: warning: found </div> at different nesting level (6) than expected (3)
 /cbmc/doc/architectural/howto.md:261: warning: end of comment block while expecting command </div>
 /cbmc/src/solvers/README.md:434: warning: Invalid list item found
-/cbmc/src/goto-instrument/wmm/event_graph.h:506: warning: The following parameters of event_grapht::explore_copy_segment(std::set< event_idt > &explored, event_idt begin, event_idt end) const are not documented:
-  parameter 'explored'
-/cbmc/src/goto-instrument/wmm/cycle_collection.cpp:149: warning: argument 'get_po_only' of command @param is not found in the argument list of event_grapht::graph_explorert::backtrack(std::set< critical_cyclet > &set_of_cycles, event_idt source, event_idt vertex, bool unsafe_met, event_idt po_trans, bool same_var_pair, bool lwfence_met, bool has_to_be_unsafe, irep_idt var_to_avoid, memory_modelt model)
-/cbmc/src/goto-instrument/wmm/event_graph.h:315: warning: The following parameters of event_grapht::graph_explorert::backtrack(std::set< critical_cyclet > &set_of_cycles, event_idt source, event_idt vertex, bool unsafe_met, event_idt po_trans, bool same_var_pair, bool lwfence_met, bool has_to_be_unsafe, irep_idt var_to_avoid, memory_modelt model) are not documented:
-  parameter 'set_of_cycles'
-  parameter 'source'
-  parameter 'vertex'
-  parameter 'unsafe_met'
-  parameter 'po_trans'
-  parameter 'same_var_pair'
-  parameter 'lwfence_met'
-  parameter 'has_to_be_unsafe'
-  parameter 'var_to_avoid'
-  parameter 'model'
-/cbmc/src/goto-instrument/wmm/goto2graph.h:260: warning: The following parameters of instrumentert::cfg_visitort::visit_cfg_function(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function, std::set< nodet > &ending_vertex) are not documented:
-  parameter 'model'
-  parameter 'no_dependencies'
-  parameter 'duplicate_body'

src/goto-instrument/wmm/cycle_collection.cpp

@@ -147,7 +147,6 @@ event_grapht::critical_cyclet event_grapht::graph_explorert::extract_cycle(
 }
 
 /// see event_grapht::collect_cycles
-/// \param get_po_only: used for po-transitivity
 bool event_grapht::graph_explorert::backtrack(
   std::set<critical_cyclet> &set_of_cycles,
   event_idt source,

src/goto-instrument/wmm/event_graph.cpp

@@ -68,6 +68,7 @@ void event_grapht::print_graph()
 
 /// copies the segment
 /// \param begin: top of the subgraph
+/// \param explored: set of segments which have already been explored
 /// \param end: bottom of the subgraph
 void event_grapht::explore_copy_segment(std::set<event_idt> &explored,
   event_idt begin, event_idt end) const

src/goto-instrument/wmm/goto2graph.cpp

@@ -145,14 +145,11 @@ unsigned instrumentert::goto2graph_cfg(
 }
 
 void instrumentert::cfg_visitort::visit_cfg_function(
-    /* value_sets and options */
     value_setst &value_sets,
     memory_modelt model,
     bool no_dependencies,
     loop_strategyt replicate_body,
-    /* function to analyse */
     const irep_idt &function,
-    /* outcoming edges */
     std::set<instrumentert::cfg_visitort::nodet> &ending_vertex)
 {
   /* flow: egraph */

src/goto-instrument/wmm/goto2graph.h

@@ -257,15 +257,19 @@ class instrumentert
     }
 
     /// TODO: move the visitor outside, and inherit
+    /// \param value_sets: Value_sets and options
+    /// \param model: Memory model
+    /// \param no_dependencies: Option to disable dependency analysis
+    /// \param duplicate_body: Control which loop body segments should
+    ///   be duplicated
+    /// \param function: Function to analyse
+    /// \param ending_vertex: Outcoming edges
     virtual void visit_cfg_function(
-      /// value_sets and options
       value_setst &value_sets,
       memory_modelt model,
       bool no_dependencies,
       loop_strategyt duplicate_body,
-      /// function to analyse
       const irep_idt &function,
-      /// outcoming edges
       std::set<nodet> &ending_vertex);
 
     bool inline local(const irep_idt &i);