Merge pull request #3388 from sonodtt/doc-day-cprover-invariant-extra-comments

Initial additional information about the invariant macros and hierarchy.

Author: sonodtt

src/util/invariant.h

@@ -82,6 +82,9 @@ Author: Martin Brain, [email protected]
 /// family of macros, allowing constructs like
 /// `INVARIANT(x==y, my_invariantt, (T1)actual1, (T2)actual2, ...)`
 ///
+/// \ref invariant_failedt is also the base class of any 'structured
+/// exceptions' - as found in file \ref base_exceptions.h
+///
 class invariant_failedt
 {
  private:
@@ -196,6 +199,9 @@ std::string get_backtrace();
 
 void report_exception_to_stderr(const invariant_failedt &);
 
+/// This function is the backbone of all the invariant types.
+/// Every instance of an invariant is ultimately generated by this
+/// function template, which is at times called via a wrapper function.
 /// Takes a backtrace, gives it to the reason structure, then aborts, printing
 /// reason.what() (which therefore includes the backtrace).
 /// In future this may throw `reason` instead of aborting.
@@ -230,8 +236,9 @@ CBMC_NORETURN
   abort();
 }
 
-/// Takes a backtrace, constructs an invariant_violatedt from reason and the
-/// backtrace, aborts printing the invariant's description.
+/// This is a wrapper function used by the macro 'INVARIANT(CONDITION, REASON)'.
+/// It constructs an invariant_violatedt from reason and the
+/// backtrace, then aborts after printing the invariant's description.
 /// In future this may throw rather than aborting.
 /// \param file : C string giving the name of the file.
 /// \param function : C string giving the name of the function.
@@ -342,6 +349,7 @@ std::string assemble_diagnostics(Diagnostics &&... args)
 }
 } // namespace detail
 
+/// This is a wrapper function, used by the macro 'INVARIANT_WITH_DIAGNOSTICS'
 template <typename... Diagnostics>
 CBMC_NORETURN void report_invariant_failure(
   const std::string &file,
@@ -387,6 +395,8 @@ CBMC_NORETURN void report_invariant_failure(
 
 // Short hand macros. The variants *_STRUCTURED below allow to specify a custom
 // exception, and are equivalent to INVARIANT_STRUCTURED.
+
+/// This macro uses the wrapper function 'invariant_violated_string'.
 #define INVARIANT(CONDITION, REASON)                                           \
   do                                                                           \
   {                                                                            \
@@ -400,6 +410,7 @@ CBMC_NORETURN void report_invariant_failure(
 /// Same as invariant, with one or more diagnostics attached
 /// Diagnostics can be of any type that has a specialisation for
 /// invariant_helpert
+/// This macro uses the wrapper function 'report_invariant_failure'.
 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...)                     \
   do                                                                           \
   {                                                                            \