1

klee 对 symbolic.c 生成文件的执行结果：

---

2

修改代码

• 头文件引用添加：

#include <klee/klee.h>

• 执行部分：

将原先的读入：

int main() {
  maze[y][x] = 'X';
  read(0, program, ITERS);
  ...
}

修改为可以进行符号执行的对象

int main() {
  maze[y][x] = 'X';
  klee_make_symbolic(program,ITERS,"program");
  ...
}

• 加入成功后添加断言：

void win() {
  printf("You win!\n");
  klee_assert(0);
  printf("Your solution: %s\n", program);
  exit(0);
}

---

执行结果

klee 对 maze.c 生成文件的执行结果，klee 生成的测试用例在 maze.c 上的执行结果：

可以看到 $306$ 个测试用例中有 $1$ 个出错

---

找到是 $143$ 号出现错误

---

查看这个错误用例的详细情况：发现它的解决方案是 sddwddddsddw

---

编译执行步骤 sddwddddsddw，复现一下该场景
可以从下面看出，这两步中出现了穿墙的问题

---

问题解决

可以看出，以上两种穿墙的情况，均符合以下代码中第二个 if 判断格子是否为空时： !((y == 2 && maze[y][x] == '|' && x > 0 && x < W)) 的触发条件

原代码：

void status() {
  if (maze[y][x] == '#') {
    win();
  }
  if (maze[y][x] != ' ' &&
        !((y == 2 && maze[y][x] == '|' && x > 0 && x < W))) {
    x = ox;
    y = oy;
  }
  if (ox == x && oy == y) {
    lose();
  }
}

于是只需将该条件删去即可
代码修改为：

void status() {
  if (maze[y][x] == '#') {
    win();
  }
  if (maze[y][x] != ' ') {
    x = ox;
    y = oy;
  }
  if (ox == x && oy == y) {
    lose();
  }
}

再次编译执行后得到：

找到 error 所在以及正确的迷宫解决方法 ssssddddwwaawwddddssssddwwww

---

3

修改代码

将原 main 函数修改为：

int main() {
    struct BST *tree = malloc(sizeof(struct BST));

    int n;
    int len = 5;
    klee_make_symbolic(&n, sizeof(n), "n");
    klee_assume(n > 0 && n <= len);

    int num[len];
    klee_make_symbolic(num, sizeof(num),"num");
    for (int i = 0; i < n; i++) {
        insert(tree, num[i]);
    }

    // Inorder traversal of the BST:
    printInorder(tree);
    printf("\n");

    for (int i = 0; i < n; i++) {
        klee_assert(search(tree, num[i]) == 1);
    }

    for (int i = 0; i < n; i += 2) {
        int deleteVal = i;
        deleteNode(tree->root, deleteVal);
    }

    for (int i = 0; i < n; i += 2) {
        klee_assert(search(tree, num[i]) == 0);
    }

    // Inorder traversal of the BST:
    printInorder(tree);
    printf("\n");
    return 0;
}

---

执行结果

执行一段时间后停止
找到问题：在 main 函数调用 deleteNode 时出错
再继续向下发现：在 main 函数执行 deleteNode 时，默认根节点不改变，导致根节点右子树为空时出错

---

问题解决

应该用 deleteNode 返回值更新根节点，删除节点的代码修改为：

	for (int i = 0; i < n; i += 2) {
        int deleteVal = num[i];
        tree->root = deleteNode(tree->root, deleteVal);
    }

执行结果如下，可以看出该问题已解决。

---

再通过直接编译执行验证问题解决情况

原代码：

for (int i = 1; i < argc; i += 2) {
        int deleteVal = i;
        deleteNode(tree->root, deleteVal);
    }

修改后：

for (int i = 1; i < argc; i += 2) {
 int deleteVal = atoi(argv[i]);
 tree->root = deleteNode(tree->root, deleteVal);
 }

执行结果如下，发现 deleteNode 错误修改完毕

---