frama-c - 有什么方法可以抛弃 frama-c 创建的替代证明义务？

Question

我目前正在玩 frama-c，我正在寻找 frama-c 如何对提供给证明者（或证明助手）的各种证明义务进行编码。在这种情况下，alt-ergo。

我想知道是否有任何特定的方法可以“转储”给 alt-ergo 的输入（假设 alt-ergo 是从 frama-c 调用的；即不是互操作）？

我想看看 C 程序属性的证明义务是如何在 alt-ergo 的“本机”输入语言中编码的。任何帮助将不胜感激。

Answer 1

该选项-wp-out <dir>允许您选择<dir>放置生成文件的目录。这些文件根据使用的内存模型（typed默认情况下）在子目录中排序。对于 Alt-Ergo，您应该找到以.ergo仅包含证明义务结尾的文件，以及以_Alt-Ergo.mlw包含证明义务的完整上下文（包括定义算术和记忆模型的公理）结尾的文件。

但是请注意，即将推出的 Frama-C 20.0 Calcium 正在引入使用 Why3 的​​ API 与证明者进行通信，因此原生 Alt-Ergo（和 Coq）输出正在慢慢被弃用。