klee check 如何验证测试通过或失败？

Question

我已经阅读了 Klee tutorial. It's pretty simple and straight forward. However, when I check files that generated by the test at KLEE generated files 上的 klee 教程，我没有找到任何文件告诉我测试是否通过？可以有两种方法来验证测试结果。

KLEE 足够聪明，知道 3 个测试用例的预期 return 值是多少
KLEE 只是将 return 值转储到文件中的某处，人类开发人员需要自己检查它们。

是这样吗？

Answer 1

Klee 不会在测试时向您提供程序运行ning 的输出，因为它正在静态分析您的代码（大多数情况下）。所以它实际上并没有运行ning 你的程序，这就是它很快的原因。如果它想要运行您的程序，则需要花费更多时间。你只需要自己运行看看输出是否符合你的预期。

Klee是测试输入生成工具，不是测试用例生成工具。区别在于测试用例既有输入也有预期输出。

Answer 2

KLEE 使用 LLVM 测试基础设施 llvm-lit 进行单元测试。命令和pass/fail检查写在注释中。

以test/Feature/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;
}

klee check 如何验证测试通过或失败？

how does klee check verify the test pass or fail?

autotest

llvm

klee