试图在 python 中用 z3 分析一些 C 程序，并遇到了指针的麻烦。我正在使用以下术语:
float * buffer = (float*)malloc(5*sizeof(float))
我将缓冲区解释为 BitVec(32) 值
所以 *buffer 应该是 Real()。
那应该没问题，但是我应该为像
*(buffer+3) or *(buffer+i)
如果我像这样索引出来，应该如何编写断言
*(buffer-1) or *(buffer+10)
最佳答案
一种解决方案是将程序堆编码为从位置到值的映射H。在Z3中，数组理论可以用来对 map 进行编码。
指针/地址是整数位置，整数算术编码指针算术；这将在您的编码中允许诸如 H(buffer + i) > 0 之类的约束。如果您要对一种 OO 语言进行编码，则可以使用该对 (接收方、字段名称) 来对地址进行编码。例如。 H(r, f) > 0 将对应于 r.f > 0。请注意，此 map 编码自然会考虑别名，例如如果 buffer1 == buffer2 和 i == 3 则 H(buffer1 + i) == H(buffer + 3)。
参见论文 Heaps and Data Structures: A Challenge for Automated Provers对基于映射的堆编码进行有趣的比较。
基于 map 的编码通常由基于验证条件的工具使用，例如 Frama-C , Dafny和 Boogie .基于符号执行的工具，如Silicon (这是 Viper verification infrastructure 的一部分)和 VeriFast通常使用不同的编码；看，例如Heap-Dependent expressions in separation logic .
关于c - 你将如何在 z3 中实现指针的取消引用，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/45690728/