我目前正在玩frama-c，我想看看frama-c是如何编码给证明人(或证明助理(的各种证明义务的。在这个例子中，alt ergo。
我想知道是否有任何特定的方法来"转储"给alt-ergo的输入(假设alt-ergo是从frama-c调用的；即不是interop(？
我想看看C程序属性的证明义务是如何在alt-ergo的"原生"输入语言中编码的。如有任何协助，我们将不胜感激。
选项-wp-out <dir>允许您选择<dir>作为将要放置生成文件的目录。这些文件根据使用中的内存模型(默认情况下为typed(在子目录中进行排序。对于Alt-Ergo，您应该找到以.ergo结尾的仅包含证明义务的文件，以及以_Alt-Ergo.mlw结尾的包含证明义务完整上下文的文件(包括定义算术和记忆模型的公理(。
然而，请注意，即将推出的Frama-C 20.0 Calcium引入了Why3的API用于与证明方进行通信，因此，原生Alt-Ergo(和Coq(输出正在慢慢被弃用。