Frama-c Magnesium:无法在Windows上执行WP插件

Question

我使用这里提供的说明安装了frama-c Magnesium版本.frama-c -version在Cygwin打印的Frama-c版本的安装和执行命令期间,我没有收到任何错误:Magnesium-20151002.但是当我-wp在一个非常小的例子上执行插件时,对于使用的目标alt-ergo,我得到以下错误:

1 [main] frama-c 8168 child_info_fork::abort: unable to map C:\cygwin\usr\local\lib\frama-c\plugins\Users.cmxs, Win32 error 998 1 [main] frama-c 7956 child_info_fork::abort: unable to map C:\cygwin\usr\local\lib\frama-c\plugins\Value.cmxs, Win32 error 998

0 [main] frama-c 300 child_info_fork::abort: unable to map C:\cygwin\usr\local\lib\frama-c\plugins\Value.cmxs, Win32 error 998 [wp] [Alt-Ergo] Goal typed_changeCase_assert_rte_signed_overflow_2 : Failed Error: Resource temporarily unavailable

值插件执行成功.我搜索了错误并找到了这篇文章.所以我也执行了rebaseall -v命令,但这也没有帮助.为了确认我的Cygwin没有损坏我再次安装了Frama-c Sodium版本并且能够成功执行WP插件.

任何人都可以帮我解决这个问题,我们希望能够在Windows上使用Frama-c Magnesium版本吗？

编辑:机器详细信息:我在计算机上和VM上都尝试过.在VM上,我执行了命令./configure && make and make install来安装frama-c Magnesium.

我在两台机器上都有32位Cygwin.两个Windows都是64位.

1. 我机器上的Ocaml版本:4.02.3,VM上的Ocaml版本:4.01.0
2. 我的机器和VM上的Cygwin版本:CYGWIN_NT-6.1-WOW64 1.7.27(0.271/5/3)2013-12-09 11:57 i686 Cygwin

Answer 1

Frama-C Magnesium 发布时，alt-ergo 1.01 还不存在。因此，当Magnesium 的 WP 手册提到与 alt-ergo 的兼容性时0.99.1+，它无法预见到与当时未来版本的 alt-ergo 会不兼容。

幸运的是，下一个版本（Aluminium）将与 alt-ergo 1.01 兼容，所以这在将来应该不是问题。

同时，您应该能够使用 alt-ergo 0.99.1。

编辑：根据错误消息和更多详细信息，它可能与您的 Cygwin 版本有关，该版本似乎相对较旧，从 2013 年开始；你的是1.7.27，而我用的是2.4.1。