c - 如何使用神器模型检查器？

Question

我一直在尝试使用DIVINE4模型检查器来验证示例 C 程序，但由于提供的教程中的冲突，我没有得到好的结果。您能推荐一些可以清楚解释这些步骤的好资源吗？(我已经彻底寻找过这个，但没有找到太多)

Answer 1

神圣manual应该涵盖您需要的大部分主题。但是，这些示例并未更新到 DIVINE 的最新版本。

这个问题可以修复。让我们以第一个示例 Airlines.cpp 为例。如果您进行以下更改:

1. 注释掉#include“divine.h”。
2. 将所有“__divine_choice”替换为“__vm_choose”。
3. 将“__divine_malloc”替换为“malloc”

您可以使用以下方式执行验证:

divine/_build.release/tools/divine verify -std=c++11 airlines.cpp