C-DbC

This module implements Design by Contract and a disciplined exception mechanism for the C language.

To install all that there is required is to copy dbc.h to a standard include directory (e.g. /usr/local/include), and both libraries files (the sequential and the POSIX thread-safe version) to a standard library directory (e.g. /usr/local/lib).

To use this library you should include dbc.h (#include <dbc.h>) and link the program with the appropriate library version (-ldbc or -lpthreaddbc). Please note that in this library DbC is defined at compile time, hence a change in the detection of assertion failures requires the recompilation of the applicable modules.

Using DbC is simply a matter of using the appropriate function -- require, ensure, invariant, check -- in the places where that meaning is expected to be verified.

This library allows also the possibility of attaching an error code (other than the internal assertion type code) to an assertion failure.  Such functions are suffixed with '_e'.

An assertion failure throws an exception (see next section), being the default behavior to create a core file (which can be read with a debugger such as gdb, to view the complete function stack trace at the time of the failure). Please note, that to create core files it might be required execute appropriate commands in the console shell (see dbc.h).

It is possible to fine-tune assertion verification using C macros (preprocessor) mechanism. To that goal, the programmer might (at a unit of compilation scope), define the following macros:

For example, to only activate preconditions, the compilation module should be compiled with DBC_PRECONDITIONS macro defined (-DDBC_PRECONDITIONS).

It is also possible to directly throw (and catch) exceptions (other than those resulting from an assertion failure). An exception is also attached to an integer value (that can be used to identify the failure source). Assertion failures also generate exception throwing (being the type of assertion part of the exception integer value).

The disciplined exception mechanism (see Eiffel) is based on a very simply (but powerful) idea: either a function succeeds or it fails, no "limbo" ambiguous state is allowed. No such simple assurance is present in try-catch exception blocks used in many programming languages (Java, C++, C#, Python, etc.), because catch blocks are allowed to filter exceptions (without any consequence on on logical control path of the algorithm as if the try block was executed normally).
One can even find such potentially disastrous usage from Java Language Specification books (and many others). The following code excerpt (wisely named BlewIt), exemplifying a first usage of the mechanism, was taken from The Java Language Specification, Java SE 7 Edition:

   class BlewIt extends Exception {
       BlewIt() { }
       BlewIt(String s) { super(s); }
   }
   class Test {
       static void blowUp() throws BlewIt { throw new BlewIt(); }

       public static void main(String[] args) {
           try {
               blowUp();
           } catch (RuntimeException r) {
               System.out.println("Caught RuntimeException");
           } catch (BlewIt b) {
               System.out.println("Caught BlewIt");
           }
       }
   }

The problem here is that one may catch an exception and, regardless of the try block intended meaning (implicitly or explicitly expressed by its postcondition), ignore it completely, allowing the program to continue to execute normally after the try/catch[/finally] instruction (in Java this problem is aggravated by the existence of checked exceptions).

If one considers that the presence of an exception (regardless of its cause) is a manifestation of a failure, then a safe try/catch[/finally] block should not be allowed to terminate normally (meaning: without an exception) if it does not execute normally its try code (which is the desired behavior). Formally, one may express that either a safe try block terminates meeting its postcondition, or it fails with an exception.

This library provides a disciplined exception handling mechanism in which it is not possible to ignore an exception. Its behavior is very simple: Either a function succeeds (meaning that it does not throw any exception), and the program is allowed to proceed; or the function fails (meaning that it throws an exception), to which the programmer has the choice of retrying the try block (in this library such a block is always a function), or (re)propagate the exception.

This behavior is implemented in C through function pointers, long-jumps, and variable arguments.

Several functions -- safe_try_catch, safe_try_catch_finally and safe_try_finally -- are provided that implement this mechanism. Depending on the function, appropriate function pointers must be passed pointing to try, catch and finally blocks (implemented as functions). Since the variable arguments C mechanism is used, other arguments (of any type desired) could also exist. Such extra arguments, when present, are passed (and shared) to all try/catch/finally functions used (which implement a simple functional closure). Unlike the body and finally functions, catch function must be augmented with a first argument in which the exception error code is (automatically) passed (to allow programming of different algorithms depending on the exception detected).

In order to this mechanism to work properly, it is necessary to encapsulate body and catch functions in equivalent variable argument functions. For example, the following body (try) and catch functions:

   void try(int i) {...}
   void catch(int value, int i) { ...}

   void try_va(va_list va)
   {
       int i = va_arg(va, int);

       try(i);
   }

   void catch_va(int value, va_list va)
   {
       int i = va_arg(va, int);

       catch(value, i);
   }

A fault tolerant scheme can then be executed simply by the invocation:

   safe_try_catch(try_va, catch_va, an_integer_expression); 

As mentioned, catch code can take into consideration the exception integer value, the type of assertion failure (if any), and even both. From an exception integer value one can extract the integer value that might be attached to it (other than the assertion type), through the macro error_mask. (Other macros exist in dbc.h to identify the assertion type and for others uses.)

To aid on the creation of va versions of try/catch/finally functions a Java's jar program -- func2va.jar -- is provided that generates them from prototyped function versions (this program was implemented with ANTLR 4).