\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{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  messages.txt  run.stats         test000002.ktest  warnings.txt
info         run.istats    test000001.ktest  test000003.ktest
\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()}.