dbc.h

Go to the documentation of this file.

#ifndef DBC_H
#define DBC_H

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include "utils.h"

#ifdef NDEBUG
#define NDEBUG_CHECKS
#define NDEBUG_PRECONDITIONS
#define NDEBUG_POSTCONDITIONS
#define NDEBUG_INVARIANTS
#endif

#ifdef DEBUG_ONLY_PRECONDITIONS
#ifdef NDEBUG_PRECONDITIONS
#undef NDEBUG_PRECONDITIONS
#endif
#ifndef NDEBUG_CHECKS
#define NDEBUG_CHECKS
#endif
#ifndef NDEBUG_POSTCONDITIONS
#define NDEBUG_POSTCONDITIONS
#endif
#ifndef NDEBUG_INVARIANTS
#define NDEBUG_INVARIANTS
#endif
#endif

// check:
#ifdef NDEBUG_CHECKS
#define check(condition, message)
#else
#ifdef EXCEPTION_POLICY
#define check(condition, message) \
   if (!(condition)) \
      throw string_concat(NULL, 0, (char*)"Assertion fail", message[0] ? (char*)": " : (char*)"", message, (char*)", assertion: \"", #condition, (char*)"\", function: \"", __FUNCTION__, (char*)"\":", int2str(__LINE__), (char*)", file: \"", __FILE__, (char*)"\"\n", NULL)
#else // EXIT_POLICY (default)

#define check(condition, message) \
   if (!(condition)) \
      do { \
         fprintf (stderr, "Assertion fail%s%s, assertion: \"%s\", function: \"%s\":%d, file: \"%s\"\n", \
                  message[0] ? ": " : "", message, #condition, __FUNCTION__, __LINE__ , __FILE__); \
         *((int*)0) = 0; \
         abort (); \
      } while (0)
#endif
#endif


// precondition:
#ifdef NDEBUG_PRECONDITIONS
#define require(condition, message)
#else
#ifdef EXCEPTION_POLICY
#define require(condition, message) \
   if (!(condition)) \
      throw string_concat(NULL, 0, (char*)"Precondition fail", message[0] ? (char*)": " : (char*)"", message, (char*)", assertion: \"", #condition, (char*)"\", function: \"", __FUNCTION__, (char*)"\":", int2str(__LINE__), (char*)", file: \"", __FILE__, (char*)"\"\n", NULL)
#else // EXIT_POLICY (default)

#define require(condition, message) \
   if (!(condition)) \
      do { \
         fprintf (stderr, "Precondition fail%s%s, assertion: \"%s\", function: \"%s\":%d, file: \"%s\"\n", \
                  message[0] ? ": " : "", message, #condition, __FUNCTION__, __LINE__ , __FILE__); \
         *((int*)0) = 0; \
         abort (); \
      } while (0)
#endif
#endif


// postcondition:
#ifdef NDEBUG_POSTCONDITIONS
#define ensure(condition, message)
#else
#ifdef EXCEPTION_POLICY
#define ensure(condition, message) \
   if (!(condition)) \
      throw string_concat(NULL, 0, (char*)"Postcondition fail", message[0] ? (char*)": " : (char*)"", message, (char*)", assertion: \"", #condition, (char*)"\", function: \"", __FUNCTION__, (char*)"\":", int2str(__LINE__), (char*)", file: \"", __FILE__, (char*)"\"\n", NULL)
#else // EXIT_POLICY (default)

#define ensure(condition, message) \
   if (!(condition)) \
      do { \
         fprintf (stderr, "Postcondition fail%s%s, assertion: \"%s\", function: \"%s\":%d, file: \"%s\"\n", \
                  message[0] ? ": " : "", message, #condition, __FUNCTION__, __LINE__ , __FILE__); \
         *((int*)0) = 0; \
         abort (); \
      } while (0)
#endif
#endif

//
// invariant:
#ifdef NDEBUG_INVARIANTS
#define invariant(condition, message)
#else
#ifdef EXCEPTION_POLICY
#define invariant(condition, message) \
   if (!(condition)) \
      throw string_concat(NULL, 0, (char*)"Invariant fail", message[0] ? (char*)": " : (char*)"", message, (char*)", assertion: \"", #condition, (char*)"\", function: \"", __FUNCTION__, (char*)"\":", int2str(__LINE__), (char*)", file: \"", __FILE__, (char*)"\"\n", NULL)
#else // EXIT_POLICY (default)

#define invariant(condition, message) \
   if (!(condition)) \
      do { \
         fprintf (stderr, "Invariant fail%s%s, assertion: \"%s\", function: \"%s\":%d, file: \"%s\"\n", \
                  message[0] ? ": " : "", message, #condition, __FUNCTION__, __LINE__ , __FILE__); \
         *((int*)0) = 0; \
         abort (); \
      } while (0)
#endif
#endif

#endif

/* ************************************************** */
/* ************************************************** */