frama-c - alt-ergo 不能通过 cygwin 在 Windows 上运行

我正在尝试使用 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)

有任何想法吗？

最佳答案

以下治疗症状:
使用带有 Windows 路径的 -wp-out 标志将解决该问题

例如

frama-c -wp -wp-print -wp-out c:/Users/userName/Desktop/tmp2 ../../cygdrive/c/Users/userName/Desktop/swap.c

关于frama-c - alt-ergo 不能通过 cygwin 在 Windows 上运行，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/25896913/