我目前正在与frama-c一起玩耍,我希望了解frama-c如何编码提供给证明者(或证明助手)的各种证明义务。在这种情况下,为alt-ergo。
我想知道是否有任何特定方法可以“转储”提供给alt-ergo的输入(假设alt-ergo是从frama-c调用的;即,不是互操作的?]
我想看看如何用alt-ergo的“本机”输入语言对C程序的属性的证明义务进行编码。任何帮助将不胜感激。
选项-wp-out <dir>
允许您选择<dir>
作为放置生成文件的目录。这些文件根据使用的内存模型(默认为typed
)在子目录中排序。对于Alt-Ergo,应该找到以.ergo
结尾的仅包含证明义务的文件,以及以_Alt-Ergo.mlw
结尾的包含证明义务的完整上下文的文件(包括定义算术和内存模型的公理)。
但是请注意,即将发布的Frama-C 20.0钙正在引入使用Why3的API来与证明者进行通信的结果,因此本机Alt-Ergo(和Coq)的输出正逐渐被弃用。