#include <string.h>
#include <stdint.h>

#include "klee.h"

// CRC-64-ECMA in https://en.wikipedia.org/wiki/Cyclic_redundancy_check
uint64_t crc64(uint64_t crc, unsigned char *buf, int len)
{
	int k;

	crc = ~crc;
	while (len--)
	{
		crc ^= *buf++;
		for (k = 0; k < 8; k++)
			crc = crc & 1 ? (crc >> 1) ^ 0xC96C5795D7870F42 : crc >> 1;
	}
	return ~crc;
}

int main()
{
#define HEAD_STR "Hello, world!.. "
#define HEAD_SIZE strlen(HEAD_STR)
#define TAIL_STR " ... and goodbye"
#define TAIL_SIZE strlen(TAIL_STR)
// first 8 bytes is a 64-bit value:
#define MID_SIZE 14
#define BUF_SIZE HEAD_SIZE+TAIL_SIZE+MID_SIZE

	char buf[BUF_SIZE];
  
        klee_make_symbolic(buf, sizeof buf, "buf");

        klee_assume (memcmp (buf, HEAD_STR, HEAD_SIZE)==0);

        klee_assume (memcmp (buf+HEAD_SIZE+MID_SIZE, TAIL_STR, TAIL_SIZE)==0);

        uint64_t mid_value=*(uint64_t*)(buf+HEAD_SIZE);

        klee_assume (crc64 (0, buf, BUF_SIZE)==mid_value);
}