// 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 <stdio.h>      // for fprintf, stderr
#include <stdbool.h>    // for _Bool, true, false
#include <stdlib.h>     // 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_