Frama-c Magnesium：无法在 Windows 上执行 WP 插件答案

【问题标题】：Frama-c Magnesium : Unable to execute WP plugin on WindowsFrama-c Magnesium：无法在 Windows 上执行 WP 插件
【发布时间】：2016-04-26 15:44:19
【问题描述】：

我使用here 提供的说明安装了 frama-c Magnesium 版本。我在安装和执行命令frama-c -versionin 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

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

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

编辑：机器详情：我在我的电脑和虚拟机上都试过了。在虚拟机上，我执行了命令./configure && make and make install 来安装frama-c Magnesium。

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

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

【问题讨论】：

您尝试了哪个版本的 alt-ergo？我想您是使用 fdopen 的 OPAM MinGW 存储库安装它的？
alt-ergo 版本是 1.01，我将它与 Frama-c Sodium 和 Magnesium 版本一起使用。我按照此处给出的说明进行操作：bts.frama-c.com/dokuwiki/…，我认为它正在使用 fdopen 的 OPAM MinGW 存储库
我使用 alt-ergo 1.01 (Signal unavailable) 得到了不同的错误消息，但使用 0.99.1 我已经能够证明一些简单的断言。 WP manual 确实提到了 alt-ergo 0.99.1+ 是兼容的，但我不确定那里的“+”表示“任何主要版本”，或者只是“0.99.1”或“0.99.2”等. 我要检查一下，但我建议尝试opam install alt-ergo.0.99.1 看看是否有帮助。
您的日志在评论中不可见，考虑编辑问题以添加 alt-ergo 的版本（这似乎与您的问题相关），然后在您尝试将其降级到 0.99 时添加日志.1.
很抱歉。我安装了 alt-ergo 0.99.1。但这无济于事。我在 alt-ergo 版本 0.99.1 中遇到了同样的错误。我认为 alt-ergo 甚至在我的情况下都不会执行，因为我在执行 -wp 插件时使用了标志 -wp-alt-ergo-opt="dfkdkskl"，这当然不是一个有效的选项。我希望从 alt-ergo 收到错误消息，但我没有。

标签： c windows frama-c

【解决方案1】：

在 Frama-C Magnesium 发布时，alt-ergo 1.01 还不存在。所以当WP manual for Magnesium提到与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。

【讨论】：

我可以在 Linux 环境中使用 alt-ergo 1.01 版和 Frama-c Magnesium。我必须使用选项-wp-alt-ergo-opt="-backward-compat" 才能使其正常工作，
我安装了 alt-ergo 0.99.1。但这无济于事。我在 alt-ergo 版本 0.99.1 中遇到了同样的错误。我认为 alt-ergo 甚至在我的情况下都不会执行，因为我在执行 -wp 插件时使用了标志 -wp-alt-ergo-opt="dfkdkskl"，这当然不是一个有效的选项。我希望从 alt-ergo 收到错误消息，但我没有。