c - Frama-c 镁 : Unable to execute WP plugin on Windows

Question

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

1 [main] frama-c 8168 child_info_fork::abort: 无法映射 C:\cygwin\usr\local\lib\frama-c\plugins\Users.cmxs，Win32 错误 998 1 [main] frama-c 7956 child_info_fork::abort: 无法映射 C:\cygwin\usr\local\lib\frama-c\plugins\Value.cmxs，Win32 错误 998

0 [main] frama-c 300 child_info_fork::abort:无法映射 C:\cygwin\usr\local\lib\frama-c\plugins\Value.cmxs，Win32 错误 998 [wp] [ Alt-Ergo] 目标 typed_changeCase_assert_rte_signed_overflow_2:失败 错误:资源暂时不可用

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

谁能帮我解决这个问题，我们希望能够在 Windows 上使用 Frama-c Magnesium 版本？

编辑: 机器详细信息: 我在我的电脑上和虚拟机上都试过了。在 VM 上，我执行命令 ./configure && make 和 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 还不存在。所以当WP manual for Magnesium提到与 alt-ergo 0.99.1+ 的兼容性，它无法预见与 alt-ergo 的 future 版本不兼容。

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

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

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