是否有任何方法可以转储frama-c创建的alt-ergo证明义务?

问题描述 投票:1回答:1

我目前正在与frama-c一起玩耍,我希望了解frama-c如何编码提供给证明者(或证明助手)的各种证明义务。在这种情况下,为alt-ergo。

我想知道是否有任何特定方法可以“转储”提供给alt-ergo的输入(假设alt-ergo是从frama-c调用的;即,不是互操作的?]

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

frama-c alt-ergo
1个回答
0
投票

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

但是请注意,即将发布的Frama-C 20.0钙正在引入使用Why3的API来与证明者进行通信的结果,因此本机Alt-Ergo(和Coq)的输出正逐渐被弃用。

© www.soinside.com 2019 - 2024. All rights reserved.