1.安装klee出现的问题：
前面都没有错，最后make check时出现：make
[1]: ***
[check-local] Error 1
网上查说make check运行时可能需要root权限。不对，make check不过对后面执行没有影响。不用管它，make check过不了对后面没有影响。
2.KLEE运行的第一个小例子——get_sign：
使用klee_make_symbolic()函数来标明一个函数是符号变量。
例如：
int a;
klee_make_symbolic(&a, sizeof(a), "a");
函数的三个参数分别指：变量的内存地址，大小，名字。
遇到问题：
1. klee get_sign.o报错找不到command：klee。原因是可执行的klee没有加入到PATH中，找到klee的可执行文件并加入到klee目录下的PATH中即可。export PATH=$PATH:your_path/klee/Release+Asserts/bin/
2.export LD_LIBRARY_PATH只是临时导入，电脑重启后失效。
3.例子中第五行#include<klee/klee.h>,gcc编译时报错找不到klee/klee.h.
解决方法一：编译时加入选项-I 指明库文件的位置
解决方法二：直接将相关库文件加入系统库文件的默认路径中。具体如下所述:
#gcc找到头文件的路径
#gcc找到头文件的路径
环境变量中的C_INCLUDE_PATH。
#g++找到头文件的路径
CPLUS_INCLUDE_PATH=$CPLUS_INCLUDE_PATH:/usr/include/libxml2:/MyLib
export CPLUS_INCLUDE_PATH
#找到动态链接库的路径
LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/MyLib
export LD_LIBRARY_PATH
#找到静态库的路径
LIBRARY_PATH=$LIBRARY_PATH:/MyLib
export LIBRARY_PATH
环境变量中的C_INCLUDE_PATH。
#g++找到头文件的路径
CPLUS_INCLUDE_PATH=$CPLUS_INCLUDE_PATH:/usr/include/libxml2:/MyLib
export CPLUS_INCLUDE_PATH
#找到动态链接库的路径
LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/MyLib
export LD_LIBRARY_PATH
#找到静态库的路径
LIBRARY_PATH=$LIBRARY_PATH:/MyLib
export LIBRARY_PATH
gcc编译时标准系统库可在目录
/usr/lib 与
/lib 中找到。klee安装后其库文件没有导入到系统库文件中（不知道为什么？），手动导入例子中需要的klee目录下的头文/件到/usr/include/下（这个位置是试验很多次得出的，导入/usr/lib/和/lib/下都不行。
总结：因为在klee大文件的目录下，层级结构是这样的：klee->include->klee->下面有很多头文件，所以为了保持目录结构的一致，也把相应的头文件导入系统库文件的/usr/include/下）。
2.第二个例子——regexp：
KLEE也会找出程序中的错误，如非法内存位置访问。这个例子中的错误不是由于程序的错误，而是我们测试驱动的错误。由于我们的符号变量re是一个字符数组，都是以'\0'结尾的，但是符号变量取到这一点，所以会报错。
对于有些复杂程序，程序分支数是无限的。可以用control+c来强制结束。也可以用选项来限制klee的运行时间和内存使用：
- -max-time=seconds: Halt execution after the given number of seconds.
- -max-forks=N: Stop forking after N symbolic branches, and run the remaining paths to termination.
- -max-memory=N: Try to limit memory consumption to N megabytes.
3.第三个例子——Solving a maze with KLEE：
是一个11*7的迷宫问题，程序中故意在迷宫的第二行开了一个后门。KLEE通过符号执行找到了所有的解（包括陷阱）。
通过这个例子可以完全看到KLEE符号执行的过程，首先是按照符号变量的size每一个字节都是符号值，然后从第一个字节开始一个一个地试验具体值（本例中实验的顺序w->a->d->s,且这4个都会试个遍，然后保存所有可行的具体值，再次基础上在再试验第二个字节，如此下去，知道实验完所有的字节，也就找到了所有的可行路径。）