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

Question

我正在使用klee生成函数的测试数据。但是克莱（Klee）生成的测试数据使我遇到了一些麻烦。

输入：

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

这是klee中的测试数据：

...
object    0: name: 'a'
object    0: size: 40
object    0: data:
'xa0xffxffxffx00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00x00'

在此测试案例中，我了解变量A的大小为40个字节。这意味着每个连续数字的每个块的每个块（例如，第一个块xa0xffxffxff代表整数）。但是， xa0xffxffxff的域名值是什么？

Answer 1

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

klee_make_symbolic（）函数，该函数采用三个参数：我们想要将其视为符号的变量（内存位置）的地址，其大小和名称（可以是任何东西）。

Answer 2

您可以通过写作：

将其传输到整数

ktest-tool --write-ints t000001.ktest