Skip to content

Instantly share code, notes, and snippets.

@Mr-Slippery
Created October 20, 2019 12:46
Show Gist options
  • Save Mr-Slippery/0bccb48150a6c4a4b35851da388c6991 to your computer and use it in GitHub Desktop.
Save Mr-Slippery/0bccb48150a6c4a4b35851da388c6991 to your computer and use it in GitHub Desktop.
Template C file for verifying an array operation using KLEE
#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;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment