KLEE如何检查测试通行证或失败

Question

我已经阅读了Klee教程的Klee教程。这非常简单明了。但是，当我检查测试生成的文件生成的文件生成的文件时，我找不到任何文件告诉我测试通过还是失败？可以有两种方法来验证测试结果。

1. klee足够聪明，可以知道3个测试用例的预期回报值

2. klee只需将返回值倾倒在文件中的某个地方，人类开发人员需要自己检查它们。

是吗？

Answer 1

klee不会为您在测试上运行程序的输出提供输出，因为它正在静态分析您的代码（大多数情况下）。因此，它实际上不是运行您的程序，这就是为什么它很快。如果要运行您的程序，将需要更多时间。您只需要自己运行它，看看输出是否是您预期的。

klee是一种测试输入生成工具，而不是测试案例生成工具。区别在于测试用例既有输入又具有预期输出。

Answer 2

klee使用LLVM测试基础结构LLVM-LIT进行单位测试。命令和通过/失败检查是在评论中写的。

以测试/功能/DoubleFree.c为例。

// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s
// RUN: test -f %t.klee-out/test000001.ptr.err
int main() {
  int *x = malloc(4);
  free(x);
  // CHECK: memory error: invalid pointer: free
  free(x);
  return 0;
}