最近在使用KLEE工具进行软件缺陷检测时发现网上对于KLEE的介绍和使用的帖子很少，因此写此帖对KLEE的安装和使用方法做简单介绍，具体使用方法可以浏览官网http://klee.github.io/
阅读本文你可以了解到：
什么是KLEE
如何安装KLEE
如何使用KLEE
什么是KLEEKLEE是一款开源的自动软件测试工具，基于LLVM编译底层基础，能够自动生成测试样例检测软件缺陷。
与junit不同的地方在于，KLEE能对c程序生成字节码.bc文件，并自动生成各类缺陷，不需要再自己编写。因而使用KLEE进行软件测试是比较轻松的方式。
如何安装KLEE OS X:因为帖主的系统环境是macOS 10.13.5，因而首先介绍macOS系统，mac上的安装十分简单，可以通过官方英文文档查看安装步骤，也可以遵循如下步骤：
在安装KLEE之前，需要先安装一个名叫Docker的软件，Docker能创建与系统其他部分隔绝的容器，可以理解为一个简单的虚拟机。利用Docker可以为KLEE开辟容器空间，在容器内可以进行自己所需的软件测试工作。
Docker安装官方文档：https://docs.docker.com/docker-for-mac/
下载地址：https://hub.docker.com/editions/community/docker-ce-desktop-mac 下载前需要登录。
下载之后拖动图标安装，与其他mac程序安装一样，不再做介绍。
可以不使用Docker而直接从git上下载KLEE，请看文档。
利用Docker安装KLEE
$ docker pull klee/klee安装完成，就这么简单。
Ubuntu:安装与上述类似，但是要注意内核版本问题，如果无法安装则重启按住shift键选择较早版本的系统启动。
如何使用KLEE首先介绍创建基本画像的方法，然后介绍官方给出的一个指导教程，最后给出程序测试实例。
创建基本画像所谓画像就是创建一个库，可以将Docker理解为一个可以运送各种物品的大货船，装有不同的物品的货箱用不同颜色标明，KLEE是其中一种物品，假设它是装食物的、蓝色的箱子，每创建一个库，就相当于货船上增加了一个蓝色的箱子。
创建临时画像。
$ docker run --rm -ti --ulimit='stack=-1:-1' klee/klee输入后进入临时画像，可以继续使用shell命令。
可以看出KLEE创建了一个叫3d开头的临时画像，画像提供了clang和LLVM工具，分别做编译c文件和将c文件转换字节码文件的工作，每个新建的画像中都有klee_build 和 klee_src两个文件夹，klee_src包含了构建KLEE的源码，klee_build是klee_src构建的工程。
我们能在klee_src中发现examples文件夹，其中包含了四个初始文件夹，分别是get_sign,islower,regexp,sort，每个文件夹里面包含一个同名c文件，是官方给出的测试代码例子，在指导教程中将会用到。
输入如下exit退出临时画像，画像自动删除。
klee@3d9471c49d85:~$ exit创建永久画像。
$ docker run -ti --name=my_first_klee_container --ulimit='stack=-1:-1' klee/klee创建了一个叫my_first_klee_container的永久画像，exit退出后可以
$ docker start -ai my_first_klee_container回到画像。
如果要删除画像，输入：
$ docker rm my_first_klee_containerubuntu在创建画像时可能会报错docker连接问题，在docker前加sudo使用管理者权限可解决。
指导教程介绍KLEE的tutorial1，教程网址：http://klee.github.io/tutorials/testing-function/
tutorial 1:
测试一个判断正负数的程序，打开前文提到的get_sign.c文件，可以看到测试函数get_sign和main函数。
#include <klee/klee.h>int get_sign(int x) { if (x == 0) return 0; if (x < 0) return -1; else return 1;} int main() { int a; klee_make_symbolic(&a, sizeof(a), "a"); return get_sign(a);}其中klee_make_symbolic是KLEE工具自带的测试函数，通过自定义的变量，不断产生值赋给a，以此完成自动生成样例功能。
编译该c文件：
$ clang -I ../../include -emit-llvm -c -g get_sign.c同目录下生成了一个get_sign.bc字节码文件，然后进行测试：
$ klee get_sign.bc可以看到输出结果：
KLEE: output directory = "klee-out-0"KLEE: done: total instructions = 31KLEE: done: completed paths = 3KLEE: done: generated tests = 3列出当前目录所有文件：
$ lsget_sign.bc get_sign.c klee-last klee-out-0其中klee-out-0是本次测试结果，klee-last是最新测试结果，每次测试后覆盖。
$ ls klee-last/assembly.ll run.istats test000002.ktestinfo run.stats test000003.ktestmessages.txt test000001.ktest warnings.txtklee-last中包含最新测试的缺陷说明和测试样例等文件。
测试实例在examples文件夹中新建一个mytest文件夹，编写一个带有软件缺陷的程序：
#include<stdio.h>#include<stdlib.h>void kleeTest(int a){int arr[10];int d[10];for (int i = 0; i < 10; i++){ //赋初始值arr[i] = i;}if (a < -50){ //求余分母为0for (int i = 0; i < 10; i++){int num = i;d[i] = arr[i] % num;}}else if(a < -25){ //除法分母为0for (int i = 0; i <= 10; i++){int num = i ;d[i] = arr[i] / num;}}else if (a < 0){ //数组越界for(int i = 0; i<= 11; i++){arr[i] = i;}}else if (a < 25){ //空指针int *a = NULL;int b = *a + 1;}else if(a < 50){ //内存泄漏free(arr);}}int main(){int n;klee_make_symbolic(&n, sizeof(n), "n");kleeTest(n);return 0;}在编写缺陷程序时，帖主尝试直接用vi编写，但是预装版的vi有输入问题，在删除之后尝试用sudo命令重装vi（文档有说明画像中有sudo命令），显示ip地址无法访问无法安装成功，估计原因是画像隔离无法联网。建议在外部编写之后复制粘贴到vi中直接保存。
现在mytest中有mytest.c文件了，跟教程一样进行如下步骤:
$ clang -I ../../include -emit-llvm -c -g mytest.c $ klee mytest.bc可以看到类似下列效果：
打开error文件查看具体缺陷。
至此，你已经掌握了KLEE的使用方法。