// File: dbc.h
// SPDX-License-Identifier: Unlicensed
//
// This is free and unencumbered software released into the public domain.
/*!
* \file dbc.h
*
* \brief This header file defines macros that implement the
* Design By Contract (DBC) protocol.
*
* The macro functions \c DBC_REQUIRE, \c DBC_ENSURE, and \c DBC_INVARIANT
* are defined.
*
* If the macro \c DBC_ALL has been defined before this header file is
* included, or none of the macros \c DBC_DISABLE, \c DBC_ENABLE_REQUIRE,
* \c DBC_ENABLE_ENSURE, or \c DBC_ENABLE_INVARIANT have been defined then all
* of the DBC-check macro functions perform the specified checks and report
* error if appropriate.
*
* If only certain macro functions are required to perform their function then
* the required macro functions can be enabled by defining the appropriate
* \c DBC_ENABLE_REQUIRE, \c DBC_ENABLE_ENSURE, and/or DBC_ENABLE_INVARIANT
* macros before including the \c dbc.h header file.
*
* \version 1.0
* \date 2023
*/
#ifndef DBC_H_
#define DBC_H_
#ifndef DBC_DISABLE
#include // for fprintf, stderr
#include // for _Bool, true, false
#include // for exit, EXIT_FAILURE
/*!
* \internal
*
* \def DBC_ALL
*
* \brief If this macro is defined then all of the \c DBC macros will be
* defined.
*
* If none of the macros \c DBC_DISABLE, \c DBC_ENABLE_REQUIRE,
* \c DBC_ENABLE_ENSURE, or \c DBC_ENABLE_INVARIANT have been defined then
* all the DBC-check macros are implicitly defined.
*
* \endinternal
*/
#if !( defined( DBC_ALL ) || defined( DBC_ENABLE_REQUIRE ) \
|| defined( DBC_ENABLE_ENSURE ) || defined( DBC_ENABLE_INVARIANT ) )
// If none of the macros that control whether or not DBC
// checks are enabled are defined then define them all
#define DBC_ALL
#define DBC_ENABLE_REQUIRE
#define DBC_ENABLE_ENSURE
#define DBC_ENABLE_INVARIANT
#endif
/*!
* \def DBC_REQUIRE( pred )
*
* \brief This macro function is used to ensure that conditions are met at
* the beginning of a function call.
*
* If the \c DBC_ENABLE_REQUIRE macro is defined then the \c DBC_REQUIRE macro
* is defined, otherwise this macro does nothing.
*
* \param [in] pred The predicate that is to be tested to ensure that it
* is true.
*/
#ifndef DBC_REQUIRE
#ifdef DBC_ENABLE_REQUIRE
#define DBC_REQUIRE( pred ) DBC_ASSERT( pred, "Precondition", #pred, \
__func__, __FILE__, __LINE__ )
#else // if DBC_REQUIRE is not defined
#define DBC_REQUIRE( ... )
#endif
#else // if DBC_REQUIRE is already defined
#error "DBC_REQUIRE already defined"
#endif
/*!
* \def DBC_ENSURE( pred )
*
* \brief This macro function is used to ensure that conditions are met at
* the end of a function call.
*
* If the \c DBC_ENABLE_ENSURE macro is defined then the \c DBC_ENSURE
* macro is defined, otherwise this macro does nothing.
*
* \param [in] pred The predicate that is to be tested to ensure that it
* is true.
*/
#ifndef DBC_ENSURE
#ifdef DBC_ENABLE_ENSURE
#define DBC_ENSURE( pred ) DBC_ASSERT( pred, "Postcondition", #pred, \
__func__, __FILE__, __LINE__ )
#else // if DBC_ENSURE is not defined
#define DBC_ENSURE( pred )
#endif
#else // if DBC_ENSURE is already defined
#error "DBC_ENSURE already defined"
#endif
/*!
* \def DBC_INVARIANT( pred )
*
* \brief This macro function is used to ensure that conditions are met at
* any point in the programs execution.
*
* If the \c DBC_ENABLE_INVARIANT macro is defined then the \c DBC_INVARIANT
* macro is defined, otherwise this macro does nothing.
*
* \param [in] pred The predicate that is to be tested to ensure that it
* is true.
*/
#ifndef DBC_INVARIANT
#if defined( DBC_ENABLE_INVARIANT )
#define DBC_INVARIANT( pred ) DBC_ASSERT( pred, "Invariant", #pred, \
__func__, __FILE__, __LINE__ )
#else // if DBC_INVARIANT is not defined
#define DBC_INVARIANT( pred )
#endif
#else // if DBC_INVARIANT is already defined
#error "DBC_INVARIANT already defined"
#endif
/*!
* \internal
*
* \def DBC_ASSERT( PRED, DBC_DESC, PRED_STR, FN_NAME, FILENAME, LINE )
*
* \brief This function is used to ensure that a condition is met.
*
* This macro function is used by all of the \c DBC-check macros.
*
* If the \p pred is not met then an error message is written to \c stderr and
* the program is exited with exit code \c EXIT_FAILURE.
*
* \param [in] pred The predicate that is to be tested to ensure that
* it is true.
* \param [in] dbc_desc The type of DBC assertion (i.e. require, ensure,
* or invariant). This parameter is used in the
* construction of the assertion failure message that
* is written to \c stderr if \p pred is not true.
* \param [in] pred_str A string representation of the \p pred that is
* being tested.
* \param [in] fn_name The name of the function where the \p pred is
* being tested.
* \param [in] filename The name of the file where the \p fn_name resides.
* \param [in] line The line number of the file where the test is
* occurring.
*
* \see DBC_REQUIRE
* \see DBC_ENSURE
* \see DBC_INVARIANT
*
* \endinternal
*/
#ifndef DBC_ASSERT
#define DBC_ASSERT( pred, dbc_desc, pred_str, fn_name, filename, line ) \
do { \
if ( !( pred ) ) { \
fprintf( stderr, \
"%s: Assertion failed: Error " \
"%s: <%s> file <%s> line %d.\n", \
dbc_desc, pred_str, fn_name, filename, line ); \
exit( EXIT_FAILURE ); \
} \
} while (0)
#else // if DBC_ASSERT is already defined
#error "DBC_ASSERT already defined"
#endif
#else // if DBC_DISABLE is defined
// Define the DBC_REQUIRE, DBC_ENSURE, DBC_INVARIANT, and DBC_ASSERT macros,
// thereby disabling all DBC-checks.
#define DBC_REQUIRE( ... )
#define DBC_ENSURE( ... )
#define DBC_INVARIANT( ... )
#define DBC_ASSERT( ... )
#endif
#endif // DBC_H_
