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

#include "klee.h"

int HTML_color(uint8_t R, uint8_t G, uint8_t B)
{
	if (R==0 && G==0 && B==0) // "black"
		return 1;

	if (R==0xFF && G==0 && B==0) // "red"
		return 2;
	
	if (R==0x0 && G==0xFF && B==0) // "green"
		return 3;
	
	if (R==0 && G==0 && B==0xFF) // "blue"
		return 4;
	
	// abbreviated hexadecimal
        // like "#123"
	if ((R>>4)==(R&0xF) && (G>>4)==(G&0xF) && (B>>4)==(B&0xF))
		return 5;

	// last resort
        // like "#123456"
	return 6;
};

int main()
{
	uint8_t R, G, B;
	klee_make_symbolic (&R, sizeof R, "R");
	klee_make_symbolic (&G, sizeof R, "G");
	klee_make_symbolic (&B, sizeof R, "B");
	
        // without passing return value out of main(), KLEE wouldn't work correctly
        // perhaps, this is how we show that the return value is used somehow
        // instead of dangling as void
	return HTML_color(R, G, B);
};