我正在尝试使用alt-ergo证明程序在frama-c上运行测试文件。但是，我得到了alt-ergo的跟随错误。所有其他frama-c检查都可以。我知道问题不在于测试文件。
------------------------------------------------------------
--- Alt-Ergo (stderr) :
------------------------------------------------------------
Fatal error: exception Sys_error("/tmp/wpf0dd65.dir/typed/test_post_2_Alt-Ergo.mlw: No such file or directory")
------------------------------------------------------------
[wp] [Alt-Ergo] Goal typed_test_post_2 : Failed
Error: Alt-Ergo exits with status [2]
我在Windows机器上，以cygwin以管理员模式执行所有安装，我得到了frama-C Neon并使用进行了安装./configure & make & make-install，安装成功（所有frama-c检查都通过了我的测试文件）
我从http://alt-ergo.ocamlpro.com/download.php获得了alt-ergo Linux x86_64二进制文件的以下版本：alt-ergo-0.95.2-x86_64 。我使用该版本，因为frama-c文档要求版本0.95。
我按照以下说明安装alt-ergo（https://www.lri.fr/~marche/MPRI-2-36-1/install.html）
安装Alt-ergo
最简单的方法是获取alt-ergo的二进制文件。下载名为“ Linux x86_64 binary”的文件，然后：
chmod +x alt-ergo-0.95.2-x86_64
sudo cp alt-ergo-0.95.2-x86_64 /usr/bin/alt-ergo
打电话时which，frama-c和alt-ergo都有正确的路径
$ which frama-c
/usr/bin/frama-c
$ which alt-ergo
/usr/bin/alt-ergo
我也安装了why3并且可以检测到ergo证明程序
$ why3 config --detect-provers
Found prover Alt-Ergo version 0.95.2, Ok.
1 provers detected and 0 provers detected with unsupported version
Save config to /home/username/.why3.conf
编辑
我用在线示例创建了以下test.mlw
type 'a set
logic add : 'a , 'a set -> 'a set
logic mem : 'a , 'a set -> prop
axiom mem_add:
forall x, y : 'a. forall s : 'a set.
mem(x, add(y, s)) <->
(x = y or mem(x, s))
logic is1, is2 : int set
logic iss : int set set
goal g:
is1 = is2 ->
mem (is1, add (is2, iss))
运行alt-ergo会导致：
alt-ergo test.mlw
File "file.mlw", line 1, characters 1-26:Valid (0.0156) (0)
有任何想法吗？
以下内容可解决这些症状：将-wp-out标志与Windows路径一起使用将解决此问题。
例如
frama-c -wp -wp-print -wp-out c:/Users/userName/Desktop/tmp2 ../../cygdrive/c/Users/userName/Desktop/swap.c
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句