@@ -199,8 +199,8 @@ std::string get_backtrace();
199
199
200
200
void report_exception_to_stderr (const invariant_failedt &);
201
201
202
- // / This class is the backbone of all the invariant types. Every instance of an
203
- // / invariant is ultimately generated by this class , which is at times called
202
+ // / This function is the backbone of all the invariant types. Every instance of an
203
+ // / invariant is ultimately generated by this function template , which is at times called
204
204
// / via a wrapper function.
205
205
// / Takes a backtrace, gives it to the reason structure, then aborts, printing
206
206
// / reason.what() (which therefore includes the backtrace).
@@ -236,7 +236,7 @@ CBMC_NORETURN
236
236
abort ();
237
237
}
238
238
239
- // / This is a wrapper class used by the macro 'INVARIANT(CONDITION, REASON)'
239
+ // / This is a wrapper function used by the macro 'INVARIANT(CONDITION, REASON)'.
240
240
// / It constructs an invariant_violatedt from reason and the
241
241
// / backtrace, then aborts after printing the invariant's description.
242
242
// / In future this may throw rather than aborting.
@@ -350,7 +350,7 @@ std::string assemble_diagnostics(Diagnostics &&... args)
350
350
} // namespace detail
351
351
352
352
353
- // / This is a wrapper class , used by the macro 'INVARIANT_WITH_DIAGNOSTICS'
353
+ // / This is a wrapper function , used by the macro 'INVARIANT_WITH_DIAGNOSTICS'
354
354
template <typename ... Diagnostics>
355
355
CBMC_NORETURN void report_invariant_failure (
356
356
const std::string &file,
0 commit comments