Postconditions in C

Recently, I've been working on some code which turns out to be particularly fiendish in the number of states it can be in, and I'm finding it hard to ensure that each method actually does exactly what it's supposed to. The problem is that the code is supposed to be multi-threaded, asynchronous, cancellable and all those buzzwords, and various methods have a number of different ways of returning results (or a lack thereof). A good example of the sort of method I mean is g_input_stream_read(): it arguably has six different ways of returning results:

  1. Returning 0 if count == 0.
  3. Returning the number of bytes successfully read.
  4. Returning 0 if EOF is reached.
  5. Return G_IO_ERROR_CANCELLED if it was cancelled before anything could be read.
  6. Returning the number of bytes read despite being cancelled.

Thankfully the first two of these are handled by GIO's wrapper around the actual implementation of the read method, but that still leaves four different ways of returning results.

One approach I've found quite useful in catch bugs is something similar to the design by contract approach of adding postconditions to the methods. Obviously, since this is C, I can't add postconditions the way DbC recommends (as formal specifications of behaviour which are separate from the implementation of that behaviour) — the best I can do is to add assertions before returning from the methods. I did look into existing solutions which would add proper support for formal specification, but they all seem to have died around 5 years ago.

So, this is the approach I've come up with. It's not brilliant, and it's a bit of a hassle to apply to every method I write, but it's definitely turned out useful for the complicated ones. Any comments about ways to improve it would be appreciated, as would pointers to existing solutions which I've managed to overlook.

static gssize
my_input_stream_subclass_read (GInputStream *stream, void *buffer, gsize count, GCancellable *cancellable, GError **error)
	/* Some vaguely realistic variables which depend on the method in question. There has to be a variable for the return value. */
	gssize length_read = -1;
	gboolean reached_eof = FALSE;

	/* We assume that there's some mechanism in place to set cancelled to TRUE if @cancellable is cancelled during a relevant period of the method's execution.
	 * We do this instead of just checking g_cancellable_is_cancelled() in the postcondition to avoid the case that the method isn't cancelled until just before the postcondition. */
	gboolean cancelled = FALSE;

	/* We use a fresh #GError so that we're guaranteed to have a #GError (since @error can be NULL) which we can examine before returning. */
	GError *child_error = NULL;

	/* Preconditions */
	g_return_val_if_fail (G_IS_INPUT_STREAM (stream), -1);
	g_return_val_if_fail (buffer != NULL, -1);
	g_return_val_if_fail (cancellable == NULL || G_IS_CANCELLABLE (cancellable), -1);
	g_return_val_if_fail (error == NULL || *error == NULL, -1);

	/* Handle one particular case */
	if (count == 0) {
		length_read = 0;
		goto done;

	/* … */

	if (some_operation_which_sets_an_error (&child_error) == FALSE) {
		/* Set up the return value for this particular error condition */
		length_read = -1;
		goto done;

	/* … */

	length_read = some_operation_which_sets_the_success_return_value (cancellable);

	if (length_read < 1 && g_cancellable_set_error_if_cancelled (cancellable, &child_error) == TRUE) {
		/* Handle cancellation by setting the return values to something else */
		length_read = -1;
		goto done;

	/* … */

	/* Unref/Free calls for various local variables could go here */

	/* Postconditions */
	g_return_val_if_fail ( (count == 0 && length_read == 0 && child_error == NULL) ||
	                      (count > G_MAXSSIZE && length_read == -1 && g_error_matches (child_error, G_IO_ERROR, G_IO_ERROR_INVALID_ARGUMENT)) ||
	                      (count > 0 && count <= G_MAXSSIZE && reached_eof == TRUE && length_read == 0 && child_error == NULL) ||
	                      (count > 0 && count <= G_MAXSSIZE && reached_eof == FALSE && length_read > 0 && child_error == NULL) ||
	                      (count > 0 && count <= G_MAXSSIZE && cancelled == TRUE && length_read == -1 && g_error_matches (child_error, G_IO_ERROR, G_IO_ERROR_CANCELLED)), -1);

	/* Move the “out” parameters to their formal parameters */
	if (child_error != NULL)
		g_propagate_error (error, child_error);

	return length_read;

The core of this approach is that there's only one return statement in the method; all other points in the method which would normally have returned now goto the end of the method, which checks the postconditions before actually returning.

This requires that the return value for the method is stored in a variable. Similarly, if the method can return a GError (or, for that matter, has any other “out” parameters), all places in the method where the GError (or other output variable) would be set have to set a local variable instead — only after the postconditions are checked can these “out” parameters be moved to their formal parameters.

As I said, this approach isn't ideal, as it involves some extra local variables, moving various things around unnecessarily, some extra goto statements, and changing the flow of the code. Additionally, it's prone to misbehaving if any of the statements in the postconditions have side-effects, either due to being function calls which have side-effects, or typos (e.g. mistyping my_return_value = -1 instead of my_return_value == -1) — a proper implementation of design by contract would not be prone to this, as the specification language it uses would most likely just be first order logic.

However, this approach does have the side effect that unreffing and freeing various variables and releasing various locks used in the method can now happen in one convenient place: just before the postcondition assertion. That might simplify memory management somewhat for some methods.

In summary, it's not a particularly elegant way to implement postconditions, but it's the best I could come up with, and I'll definitely be using it in the more complex code I write in future. Any comments, corrections or suggestions for improvements are more than welcome.

Update: added a missing child_error != NULL check before the g_propagate_error() call.

3 thoughts on “Postconditions in C

  1. Benjamin Otte

    The obvious first thing to do here is to refactor that code into two functions, the one checking pre- and postconditions and the one actually doing the work. That way you get rid of the goto requirement and can actually use return. And you don't get the problem that somebody adds a new path that just returns by accident. So code would look like this:

    static int
    do_frobnicate (void *args)
    /* actually do stuff here */

    frobnicate (void *args)
    int result;

    g_return_val_if_fail (preconditions);

    result = do_frobnicate (args);

    g_assert (postconditions);

    return result;

    1. Philip Withnall Post author

      That makes sense. I suppose the disadvantage of doing it this way, though, is that the implementation of the method is then moved away from its API documentation, albeit by only a small distance.

  2. Kim Gräsman

    My first instinct was to do it the other way around -- extract a function to check the post-conditions, and return the actual value;

    static int frobnicate(...)
    /* do stuff here */
    return frobnicate_check_postconditions(... postconditions ...);

    int frobnicate_check_postconditions(int retval, ...)
    return retval;

    Not sure if that makes sense, but it would sort of inline the postcondition check with the return statement.

Comments are closed.