c - 如何通过Boogie验证VCC生成的Boogie程序？

我试着运行VCC来验证C程序。我对VCC制作的中级Boogie程序很感兴趣（因为我想在那里插入一些东西）。为此，VCC提供了/t选项。然而，当我试图在生成的BoGee程序上运行BooGee时，BoGee存在并抱怨了很多错误，这些错误分为三类（以下是我的C代码中的例子）：
Error: undeclared identifier: $arch_ptr_size
Error: undeclared type: $ctype
Error: use of undeclared function: $in_range_i4
我想验证的C程序很简单（见下文）。VCC验证它没有问题。

#include <vcc.h>

int main() {
    int i = 0;
    _(assert i == 0)
}

我做错什么了？我错过了布吉的选择吗？

最佳答案

解决方案是用附加文件Vcc3Prelude.bpl调用Boggie。

关于c - 如何通过Boogie验证VCC生成的Boogie程序？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/32707520/