有什么方法可以丢弃frama-c创建的alt-ergo证明义务吗？

Question

我目前正在使用frama-c，我想看看frama-c是如何对给予证明者(或证明助手)的各种证明义务进行编码的。在本例中，使用alt-ergo组合键。

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

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

Answer 1

选项-wp-out <dir>允许您选择<dir>作为放置生成的文件的目录。这些文件根据所使用的内存模型(默认情况下为typed)被排序在子目录中。对于Alt-Ergo，您应该发现以.ergo结尾的文件只包含证明义务，以_Alt-Ergo.mlw结尾的文件包含证明义务的完整上下文(包括定义算法和内存模型的公理)。

然而，请注意，即将发布的Frama-C 20.0钙引入了Why3的API用于与证明者通信，因此，本地Alt-Ergo (和Coq)输出正在慢慢被弃用。