diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt index df36e3d3c7b..249522300b3 100644 --- a/scripts/expected_doxygen_warnings.txt +++ b/scripts/expected_doxygen_warnings.txt @@ -19,21 +19,3 @@ /cbmc/doc/architectural/howto.md:260: warning: found at different nesting level (6) than expected (3) /cbmc/doc/architectural/howto.md:261: warning: end of comment block while expecting command /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' diff --git a/src/goto-instrument/wmm/cycle_collection.cpp b/src/goto-instrument/wmm/cycle_collection.cpp index 24bceab723c..5d7a919677d 100644 --- a/src/goto-instrument/wmm/cycle_collection.cpp +++ b/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 &set_of_cycles, event_idt source, diff --git a/src/goto-instrument/wmm/event_graph.cpp b/src/goto-instrument/wmm/event_graph.cpp index bff690bd15b..575a3fffcd0 100644 --- a/src/goto-instrument/wmm/event_graph.cpp +++ b/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 &explored, event_idt begin, event_idt end) const diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index bd9e179ea42..12a6efcf62d 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/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 &ending_vertex) { /* flow: egraph */ diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-instrument/wmm/goto2graph.h index bf1cb30693e..c4d65822de6 100644 --- a/src/goto-instrument/wmm/goto2graph.h +++ b/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 &ending_vertex); bool inline local(const irep_idt &i);