原文（http://klee.github.io/tutorials/testing-function/），这个实例用来引导你完成一个最简单的测试。
1 下面是一个待测试的函数，
int get_sign(int x) { if (x == 0) return 0;
if (x < 0) return -1; else return 1;}
这个函数就是根据输入的x，返回-1\0\1表示x的符号。
2 符号化输入
为了利用KLEE测试这个函数，首先需要设置符号化输入，也就是把输入变量符号化。这里用到 klee_make_symbolic() 函数，该函数输入三个参数，分别是变量地址、变量大小、变量名（这个名可以自己随便取，就是用作标识）。之后设置一个main函数，调用klee-make-symbolic函数，再利用符号化的输入变量调用所要测试的函数get_sign。具体main函数的定义如下：
int main() { int a; klee_make_symbolic(&a, sizeof(a), "a"); return get_sign(a);}
3 编译程序生成LLVM bitcode
KLEE的分析是基于LLVM bitcode的，所以首先需要用llvm-gcc编译c文件生成文件，命令如下：
$ llvm-gcc --emit-llvm -c -g get_sign.c
生成get_sign.o文件，-g参数用于在编译中加入debug信息，以便于产生源代码级别的程序信息。同时编译中不要使用优化设置的参数。
4 运行KLEE分析程序
$ klee get_sign.o
可以得到如下的输出：
KLEE: output directory = "klee-out-0"
KLEE: done: total instructions = 51 KLEE: done: completed paths = 3 KLEE: done: generated tests = 3
从中可以看出，该测试函数有3条路径，并且为每一条路径都生成了一个测试例。KLEE执行输出信息都在文件klee-out-N中，不过最近一次的执行生成的目录由klee-last快捷方式指向。
查看生成的文件：
$ ls klee-last/ assembly.ll run.istats test000002.ktest info run.stats test000003.ktest messages.txt test000001.ktest warnings.txt
5 KLEE生成的测试例查看
扩展名为.ktest的都是生成的测试例，这个程序有三条path，所以三个测试例，这些文件都是二进制代码，可以用ktest-tool命令查看，具体如下：
$ ktest-tool --write-ints klee-last/test000001.ktest ktest file : 'klee-last/test000001.ktest' args : ['get_sign.o'] num objects: 1 object 0: name: 'a' object 0: size: 4 object 0: data: 1
$ ktest-tool --write-ints klee-last/test000002.ktest ... object 0: data: -2147483648
$ ktest-tool --write-ints klee-last/test000003.ktest ... object 0: data: 0
很明显的可以看到，每一个路径对应的输入变量值，分别是1, -2147483648, 0。
6 利用测试例运行程序
用生成的测试例作为输入运行程序，命令如下：
$ export LD_LIBRARY_PATH=path-to-klee-root/Release+Asserts/lib/:$LD_LIBRARY_PATH
#LD_LIBRARY_PATH中的path-to-klee-root需要用具体的路径代替，后面的也一样 $ gcc -L path-to-klee-root/Release+Asserts/lib/ get_sign.c -lkleeRuntest
#gcc编译生成a.out，一个可执行程序，然后用下面的方式指定其输入为test000001.ktest。
$ KTEST_FILE=klee-last/test000001.ktest ./a.out $ echo $?
#查看返回值 1 $ KTEST_FILE=klee-last/test000002.ktest ./a.out $ echo $?
#255实际上对应的是-1 255 $ KTEST_FILE=klee-last/test000003.ktest ./a.out $ echo $? 0
2015-1-26: While running a.out, you can run ./a.out directly. klee will ask you input .ktest file.
