Skip to content

Commit 3a18c51

Browse files
author
John Nonweiler
committed
Update parameter documentation
Fix Doxygen warnings by adding documentation for some undocumented parameters. Also change documentation format to match the coding standard (including removing comments on parameters in goto2graph.cpp which duplicate documentation in goto2graph.h).
1 parent 9296bc3 commit 3a18c51

File tree

4 files changed

+8
-12
lines changed

4 files changed

+8
-12
lines changed

scripts/expected_doxygen_warnings.txt

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,3 @@
1919
/cbmc/doc/architectural/howto.md:260: warning: found </div> at different nesting level (6) than expected (3)
2020
/cbmc/doc/architectural/howto.md:261: warning: end of comment block while expecting command </div>
2121
/cbmc/src/solvers/README.md:434: warning: Invalid list item found
22-
/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:
23-
parameter 'explored'
24-
/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:
25-
parameter 'model'
26-
parameter 'no_dependencies'
27-
parameter 'duplicate_body'

src/goto-instrument/wmm/event_graph.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,7 @@ void event_grapht::print_graph()
6868

6969
/// copies the segment
7070
/// \param begin: top of the subgraph
71+
/// \param explored: set of segments which have already been explored
7172
/// \param end: bottom of the subgraph
7273
void event_grapht::explore_copy_segment(std::set<event_idt> &explored,
7374
event_idt begin, event_idt end) const

src/goto-instrument/wmm/goto2graph.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -145,14 +145,11 @@ unsigned instrumentert::goto2graph_cfg(
145145
}
146146

147147
void instrumentert::cfg_visitort::visit_cfg_function(
148-
/* value_sets and options */
149148
value_setst &value_sets,
150149
memory_modelt model,
151150
bool no_dependencies,
152151
loop_strategyt replicate_body,
153-
/* function to analyse */
154152
const irep_idt &function,
155-
/* outcoming edges */
156153
std::set<instrumentert::cfg_visitort::nodet> &ending_vertex)
157154
{
158155
/* flow: egraph */

src/goto-instrument/wmm/goto2graph.h

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -257,15 +257,19 @@ class instrumentert
257257
}
258258

259259
/// TODO: move the visitor outside, and inherit
260+
/// \param value_sets: Value_sets and options
261+
/// \param model: Memory model
262+
/// \param no_dependencies: Option to disable dependency analysis
263+
/// \param duplicate_body: Control which loop body segments should
264+
/// be duplicated
265+
/// \param function: Function to analyse
266+
/// \param ending_vertex: Outcoming edges
260267
virtual void visit_cfg_function(
261-
/// value_sets and options
262268
value_setst &value_sets,
263269
memory_modelt model,
264270
bool no_dependencies,
265271
loop_strategyt duplicate_body,
266-
/// function to analyse
267272
const irep_idt &function,
268-
/// outcoming edges
269273
std::set<nodet> &ending_vertex);
270274

271275
bool inline local(const irep_idt &i);

0 commit comments

Comments
 (0)