alt-ergo不通过cygwin在windows上运行。

Question

我正在用alt-ergo测试程序在frama-c上运行一个测试文件。然而，我得到了下面的alt-ergo错误。所有其他的夫人-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检查通过了我的测试文件)。

我得到了下面版本的alt二进制文件:alt 0.95.2-x86_64来自x86_64。我使用了这个版本，因为frama文档要求版本为0.95。

我使用了以下说明来安装alt-ergo (https://www.lri.fr/~marche/MPRI-2-36-1/install.html)

安装Alt-ergo

最简单的方法是获取alt-ergo的二进制文件。下载名为"Linux x86_64二进制文件“的文件：

   chmod +x alt-ergo-0.95.2-x86_64 
   sudo cp alt-ergo-0.95.2-x86_64 /usr/bin/alt-ergo

当调用which时，frama和alt有正确的路径。

$ 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)

有什么想法吗？

Answer 1

以下处理症状:使用带windows路径的-wp-out标志将解决此问题。

例如

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

Answer 2

你能把下面的例子放在"file.mlw“中吗？

goal hello_world: 1+1 = 2

然后，尝试通过提供"file.mlw“作为输入来执行Windows和/或Cygwin二进制文件