#include <stdlib.h>
#include <stdbool.h>
#include <stddef.h>

typedef struct { size_t length; char* buffer; } strbuf;

strbuf* strbuf_allocate(size_t length) {
  strbuf* str = malloc(sizeof(strbuf));
  if (str == NULL) return NULL;
  str->length = length;
  str->buffer = malloc(length);
  return str;
}

bool strbuf_is_valid(strbuf* str) {
  if (str == NULL) return false;
  if (str->buffer == NULL) return false;
  return true;
}

char cache;
int counter;

char cache_fifth_char(strbuf* str)
  __CPROVER_requires(strbuf_is_valid(str))
  __CPROVER_requires(str->length > 4)
  __CPROVER_ensures(strbuf_is_valid(str))
  __CPROVER_ensures(str->length > 4)
  __CPROVER_assigns(cache)

  __CPROVER_ensures(cache == __CPROVER_return_value)
  __CPROVER_ensures(counter == __CPROVER_old(counter) + 1)
  __CPROVER_assigns(counter)
{
  counter = counter + 1;
  cache = str->buffer[4];
  return str->buffer[4];
}

main() {
  size_t len;
  strbuf* str = strbuf_allocate(len);

  cache_fifth_char(str);
}