Document cover functions

Author: peterschrammel

src/goto-instrument/cover.cpp

@@ -13,20 +13,18 @@ Date: May 2016
 
 #include "cover.h"
 
-#include <iterator>
-#include <unordered_set>
-
 #include <util/config.h>
-#include <util/cprover_prefix.h>
-#include <util/format_number_range.h>
 #include <util/message.h>
-#include <util/prefix.h>
 #include <util/make_unique.h>
 
 #include "cover_basic_blocks.h"
 #include "cover_filter.h"
 #include "cover_instrument.h"
 
+/// Applies instrumenters to given goto program
+/// \param goto_program: the goto program
+/// \param instrumenters: the instrumenters
+/// \param message_handler: a message handler
 void instrument_cover_goals(
   goto_programt &goto_program,
   const cover_instrumenterst &instrumenters,
@@ -40,6 +38,11 @@ void instrument_cover_goals(
   instrumenters(goto_program, basic_blocks);
 }
 
+/// Instruments goto program for a given coverage criterion
+/// \param symbol_table: the symbol table
+/// \param goto_program: the goto program
+/// \param criterion: the coverage criterion
+/// \param message_handler: a message handler
 void instrument_cover_goals(
   const symbol_tablet &symbol_table,
   goto_programt &goto_program,
@@ -55,6 +58,10 @@ void instrument_cover_goals(
   instrument_cover_goals(goto_program, instrumenters, message_handler);
 }
 
+/// Create and add an instrumenter based on the given criterion
+/// \param criterion: the coverage criterion
+/// \param symbol_table: the symbol table
+/// \param goal_filters: goal filters to discard certain goals
 void cover_instrumenterst::add_from_criterion(
   coverage_criteriont criterion,
   const symbol_tablet &symbol_table,
@@ -100,6 +107,9 @@ void cover_instrumenterst::add_from_criterion(
   }
 }
 
+/// Parses a coverage criterion
+/// \param criterion_string: a string
+/// \return a coverage criterion or throws an exception
 coverage_criteriont
 parse_coverage_criterion(const std::string &criterion_string)
 {
@@ -131,6 +141,11 @@ parse_coverage_criterion(const std::string &criterion_string)
   return c;
 }
 
+/// Applies instrumenters to given goto functions
+/// \param goto_functions: the goto functions
+/// \param instrumenters: the instrumenters
+/// \param function_filters: function filters to discard certain functions
+/// \param message_handler: a message handler
 void instrument_cover_goals(
   goto_functionst &goto_functions,
   const cover_instrumenterst &instrumenters,
@@ -146,6 +161,11 @@ void instrument_cover_goals(
   }
 }
 
+/// Instruments goto functions based on given command line options
+/// \param cmdline: the command line
+/// \param symbol_table: the symbol table
+/// \param goto_functions: the goto functions
+/// \param message_handler: a message handler
 bool instrument_cover_goals(
   const cmdlinet &cmdline,
   const symbol_tablet &symbol_table,
@@ -258,6 +278,10 @@ bool instrument_cover_goals(
   return false;
 }
 
+/// Instruments a goto model based on given command line options
+/// \param cmdline: the command line
+/// \param goto_model: the goto model
+/// \param message_handler: a message handler
 bool instrument_cover_goals(
   const cmdlinet &cmdline,
   goto_modelt &goto_model,

src/goto-instrument/cover.h

@@ -29,7 +29,7 @@ enum class coverage_criteriont
   PATH,
   MCDC,
   ASSERTION,
-  COVER
+  COVER // __CPROVER_cover(x) annotations
 };
 
 void instrument_cover_goals(