#include <string.h> // memcpy
#include <stdlib.h> //malloc
#include <stdint.h> //uint8_t and friends

struct Data
{
	// Luminance buffer
	uint8_t* mYChannel;
	int32_t mYStride;
	int32_t mYSize_height;
	// Chroma buffers
	uint8_t* mCbChannel;
	uint8_t* mCrChannel;
	int32_t mCbCrStride;
	int32_t mCbCrSize_height;
};



void
CopyPlane(uint8_t *aDst, const uint8_t *aSrc,
	const int32_t height, int32_t aStride)
{
	memcpy(aDst, aSrc, height * aStride);
}

void bugFunc(struct Data* aData)
{
	// overflow
	size_t size = aData->mCbCrStride * aData->mCbCrSize_height * 2 +
		aData->mYStride * aData->mYSize_height;

	// get new buffer
	uint8_t* mBuffer = (uint8_t*)malloc(size);
	if (!mBuffer)
		return;

	aData->mYChannel = mBuffer;
	aData->mCbChannel = aData->mYChannel + aData->mYStride * aData->mYSize_height;
	aData->mCrChannel = aData->mCbChannel + aData->mCbCrStride * aData->mCbCrSize_height;

	CopyPlane(aData->mYChannel, aData->mYChannel, aData->mYSize_height, aData->mYStride);
	CopyPlane(aData->mCbChannel, aData->mCbChannel, aData->mCbCrSize_height, aData->mCbCrStride);
	CopyPlane(aData->mCrChannel, aData->mCrChannel, aData->mCbCrSize_height, aData->mCbCrStride);
}


//cbmc cve-2017-5428.c --function main --bounds-check --pointer-check
int main(int argc, char** argv)
{
	struct Data test;
	test.mCbCrStride = 0x20000000;
	test.mCbCrSize_height = 4;
	test.mYStride = 0x200;
	test.mYSize_height = 1;

	bugFunc(&test);
	return 1;
}