unit-testing - 了解数组或指针的 KLEE 测试数据

Question

我正在使用 KLEE 生成功能测试数据。但是KLEE生成的测试数据让我有些烦恼。

输入：

void arrange(int a[]) {
    ...
}

这是KLEE中的测试数据：

...
object    0: name: 'a'
object    0: size: 40
object    0: data:
'\xa0\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'

在这个测试用例中，我了解到变量 a 的大小是 40 字节。意思是每块有四个连续数（例如，第一个块\xa0\xff\xff\xff代表一个整数）。然而，什么是货币价值\xa0\xff\xff\xff？

Answer 1

您可以通过编写将其转换为整数：

ktest-tool --write-ints t000001.ktest

Answer 2

对于 KLEE，它只是一个内存块。

klee_make_symbolic() 函数，它接受三个参数：我们要视为符号的变量（内存位置）的地址、它的大小和一个名称（可以是任何东西）。