Merge pull request #4078 from romainbrenguier/doc/show-program

Document show_program and show_vcc functions [DOC-144]

Author: tautschnig

src/goto-symex/show_program.h

@@ -15,6 +15,14 @@ Author: Daniel Kroening, [email protected]
 class namespacet;
 class symex_target_equationt;
 
+/// Print the steps of \p equation on the standard output.
+///
+/// For each step, prints the location, then if the step is an assignment,
+/// assertion, assume, constraint, shared read or shared write:
+/// prints an instruction counter, followed by the instruction type, and the
+/// current guard if it is not equal to true.
+/// \param ns: namespace
+/// \param equation: SSA form of the program
 void show_program(const namespacet &ns, const symex_target_equationt &equation);
 
 #endif // CPROVER_GOTO_SYMEX_SHOW_PROGRAM_H

src/goto-symex/show_vcc.cpp

@@ -23,9 +23,11 @@ Author: Daniel Kroening, [email protected]
 #include <util/json_irep.h>
 #include <util/ui_message.h>
 
-void show_vcc_plain(
-  messaget::mstreamt &out,
-  const symex_target_equationt &equation)
+/// Output equations from \p equation in plain text format to the given output
+/// stream \p out.
+/// Each equation is prefixed by a negative index, formatted `{-N}`
+static void
+show_vcc_plain(messaget::mstreamt &out, const symex_target_equationt &equation)
 {
   bool has_threads = equation.has_threads();
   bool first = true;
@@ -99,9 +101,16 @@ void show_vcc_plain(
   }
 }
 
-void show_vcc_json(
-  std::ostream &out,
-  const symex_target_equationt &equation)
+/// Output equations from \p equation in the JSON format to the given output
+/// stream \p out.
+/// The format is an array `vccs`, containing fields:
+///   - constraints, which is an array containing the constraints which apply
+///     to that equation
+///   - expression, a string containing the formatted expression
+///   - sourceLocation (optional), the corresponding location in the program
+///   - comment (optional)
+static void
+show_vcc_json(std::ostream &out, const symex_target_equationt &equation)
 {
   json_objectt json_result;
 

src/goto-symex/show_vcc.h

@@ -17,6 +17,12 @@ Author: Daniel Kroening, [email protected]
 class optionst;
 class symex_target_equationt;
 
+/// Output equations from \p equation to a file or to the standard output.
+/// The name of the output file is given by the `outfile` option from
+/// \p options, the standard input is used if it is not provided.
+/// The format is either JSON or plain text depending on \p ui_message_handler;
+/// XML is not supported.
+/// See \link show_vcc_json \endlink and \link show_vcc_plain \endlink
 void show_vcc(
   const optionst &options,
   ui_message_handlert &ui_message_handler,