gistfile1.c

#include <stdlib.h>
#include "klee/klee.h"

struct Node {
  int value;
  struct Node *next;
};

struct Node *symbolic() {
  int isNull = klee_range(0, 2, "isNull");
  if (isNull) {
    return NULL;
  } else {
    struct Node *next = symbolic();
    int value = klee_int("value");
    struct Node *this = malloc(sizeof(struct Node));
    this->value = value;
    this->next = next;
    return this;
  }
}

int head(struct Node *list) {
  klee_assert(list != NULL);
  return list->value;
}

int main() {
  struct Node *l = symbolic();

  klee_assert(l != NULL);
  klee_assert(head(l) == l->value);

  return 0;
}