#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;

void 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)
{
  cache = str->buffer[4];
}

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

  cache_fifth_char(str);
}