Template C file for verifying an array operation using KLEE

klee_template.c

#ifdef KLEE
#include <klee/klee.h>
#include <assert.h>
#endif

#include <stdbool.h>

#ifndef KLEE
#include <stdio.h>
#endif

static bool pre_condition(const int array[], /*@unused@*/ size_t n)
{
    return (0 == array[0]);
}

static void operation(int array[], size_t n)
{
    size_t i;

    for (i = 1; i < n; ++i) {
        array[i] = 1;
    }

    array[0]++;
}

static bool post_condition(const int array[], size_t n) {
    size_t i;

    for (i = 0; i < n; ++i) {
        if (1 != array[i]) {
            return false;
        }
    }
    return true;
}

#ifndef KLEE
static void print(const int array[], size_t n)
{
    size_t i;

    for (i = 0; i < n; ++i) {
        printf("%d ", array[i]);
    }
    printf("\n");
}
#endif

int main(/*@unused@*/ int argc, /*@unused@*/ char *argv[])
{
    const size_t N = 10;
    int array[N] = {0};
    bool pre_cond;

#ifdef KLEE
    klee_make_symbolic(array, sizeof array, "array");
#endif

    pre_cond = pre_condition(array, N);

    operation(array, N);

#ifdef KLEE
    // pre-conditions + code (operation(...)) imply the post-conditions
    klee_assert(post_condition(array, N) || !pre_cond);
#endif

#ifndef KLEE
    print(array, N);
#endif

    return 0;
}