\myheading{Unit test: HTML/CSS color}

The most popular ways to represent HTML/CSS color is by English name (e.g., ``red'')
and by 6-digit hexadecimal number (e.g., ``\#0077CC'').

There is a third, less popular way: if each byte in hexadecimal number has two doubling digits,
it can be \emph{abbreviated}, thus, 
``\#0077CC'' can be written just as ``\#07C''.

Let's write a function that identify a way of color encoding.
1) color name (if possible, first priority);
2) 3-digit hexadecimal form (if possible, second priority);
3) or as 6-digit hexadecimal form (as a last resort).

\lstinputlisting{KLEE/color.c}

There are 6 possible paths in function, and let's see, if KLEE could find them all?
It's indeed so:

\begin{lstlisting}
% clang -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -I /tmp/klee_src/include/klee/ color.c

% klee --libc=uclibc --optimize color.bc
...
KLEE: done: total instructions = 12232
KLEE: done: completed paths = 8
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 8
...
\end{lstlisting}

So there are 8 paths:

\begin{lstlisting}
% ls klee-last
assembly.ll   run.istats           test000001.ktest  test000004.ktest  test000007.ktest
info          run.stats            test000002.ktest  test000005.ktest  test000008.ktest
messages.txt  solver-queries.smt2  test000003.ktest  test000006.ktest  warnings.txt
\end{lstlisting}

Let's list all 8 test cases:

\begin{lstlisting}
% ktest-tool klee-last/test000001.ktest | grep hex
object 0: hex : 0x00
object 1: hex : 0x00
object 2: hex : 0x00
% ktest-tool klee-last/test000002.ktest | grep hex
object 0: hex : 0xff
object 1: hex : 0x00
object 2: hex : 0x00
% ktest-tool klee-last/test000003.ktest | grep hex
object 0: hex : 0x00
object 1: hex : 0xff
object 2: hex : 0x00
% ktest-tool klee-last/test000004.ktest | grep hex
object 0: hex : 0x00
object 1: hex : 0x00
object 2: hex : 0xff
% ktest-tool klee-last/test000005.ktest | grep hex
object 0: hex : 0x01
object 1: hex : 0x01
object 2: hex : 0x01
% ktest-tool klee-last/test000006.ktest | grep hex
object 0: hex : 0x00
object 1: hex : 0x00
object 2: hex : 0x01
% ktest-tool klee-last/test000007.ktest | grep hex
object 0: hex : 0x00
object 1: hex : 0x01
object 2: hex : 0x00
% ktest-tool klee-last/test000008.ktest | grep hex
object 0: hex : 0x11
object 1: hex : 0x00
object 2: hex : 0x00
\end{lstlisting}

1st test for black, 2nd/3rd/4th tests --- red/green/blue.

5th/6th/7th tests --- \emph{full} 6-nibble hex code.

8th test --- \emph{abbreviated} 3-nibble hex code.

The test set could be a bit shorter (6 against 8), but this is not bad too.