Skip to content

Fix Doxygen warnings in goto-instrument/wmm folder #3430

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Nov 16, 2018
Merged

Fix Doxygen warnings in goto-instrument/wmm folder #3430

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9296bc3
Remove comment about non-existent parameter
Nov 15, 2018
3a18c51
Update parameter documentation
Nov 16, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 0 additions & 18 deletions scripts/expected_doxygen_warnings.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'
1 change: 0 additions & 1 deletion src/goto-instrument/wmm/cycle_collection.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
1 change: 1 addition & 0 deletions src/goto-instrument/wmm/event_graph.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 0 additions & 3 deletions src/goto-instrument/wmm/goto2graph.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -145,14 +145,11 @@ unsigned instrumentert::goto2graph_cfg(
}

void instrumentert::cfg_visitort::visit_cfg_function(
/* value_sets and options */
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do these comments need to be removed? Surely Doxygen should just be ignoring these?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, apologies - I see they are replaced by Doxygen on the declaration instead. Ignore me :-)

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 */
Expand Down
10 changes: 7 additions & 3 deletions src/goto-instrument/wmm/goto2graph.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down