\myheading{Unit test: strcmp() function}

The standard \TT{strcmp()} function from C library can return 0, -1 or 1, depending of comparison result.

Here is my own implementation of \TT{strcmp()}:

\lstinputlisting[basicstyle=\ttfamily\small]{KLEE/strcmp.c}

Let's find out, if KLEE is capable of finding all three paths?
I intentionally made things simpler for KLEE by limiting input arrays
to two 2 bytes or to 1 character + terminal zero byte.

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

% klee --libc=uclibc --optimize strcmp.bc
KLEE: done: completed paths = 3
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 3

% ls klee-last
assembly.ll
info
messages.txt
run.istats
run.stats
test000001.ktest
test000002.ktest
test000003.ktest
warnings.txt
\end{lstlisting}

These are the input values for each path inside of my implementation of \TT{strcmp()}:

\begin{lstlisting}
% ktest-tool klee-last/test000001.ktest | grep data
object 0: data: b'a\x00'
object 1: data: b'c\x00'

% ktest-tool klee-last/test000002.ktest | grep data
object 0: data: b'a\x00'
object 1: data: b'a\x00'

% ktest-tool klee-last/test000003.ktest | grep data
object 0: data: b'c\x00'
object 1: data: b'a\x00'
\end{lstlisting}

1st is if first argument (``a'') is lesser than the second (``c''),
2nd is if they are equal (``a'' and ``a''),
3rd is fi first argument (``c'') is greater than the second (``a'').

Using these 3 test cases, we've got full coverage of our (toy) implementation of \TT{strcmp()}.

