Document show_vcc function

No functional change.

Author: romainbrenguier

src/goto-symex/show_vcc.cpp

@@ -23,6 +23,9 @@ Author: Daniel Kroening, [email protected]
 #include <util/json_irep.h>
 #include <util/ui_message.h>
 
+/// 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)
 {
@@ -98,6 +101,14 @@ show_vcc_plain(messaget::mstreamt &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)
 {

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,