如何在 Manjaro 18.1.5 上安装 Frama-C？

Question

我正在尝试在我的 manjaro 18.1.5 发行版上安装 frama-c，但无论我尝试什么，我总是遇到错误。

首先我尝试通过 AUR 安装，它似乎可以工作，但是当我尝试从 gui 打开一个文件时，它失败并显示类似“无效的用户输入”之类的信息，即使我使用的文件适用于已知良好的安装。

编辑：这是该文件的错误输出：

[kernel] Parsing max.c (with preprocessing)
[kernel:annot-error] max.c:2: Warning: 
  unbound logic variable INT_MIN. Ignoring logic specification of function max
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "max.c" that has errors. Add '-kernel-msg-key pp'
  for preprocessing command.

然后我尝试使用 opam 安装它，所以我首先尝试使用 depext 安装依赖项，但它没有安装任何东西，然后当我尝试安装 frama-c 时，它失败并出现以下错误：

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of frama-c failed at
        "/home/benoit/.opam/opam-init/hooks/sandbox.sh build make -j7".

#=== ERROR while compiling frama-c.20.0 =======================================#
# context     2.0.5 | linux/x86_64 | ocaml-system.4.09.0 | https://opam.ocaml.org#2d21a0b6
# path        ~/.opam/default/.opam-switch/build/frama-c.20.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -j7
# exit-code   2
# env-file    ~/.opam/log/frama-c-4880-6d07ae.env
# output-file ~/.opam/log/frama-c-4880-6d07ae.out
### output ###
# [...]
# Ocamlopt     src/plugins/value/legacy/eval_terms.cmx
# Ocamlopt     src/plugins/value/domains/cvalue/cvalue_transfer.cmx
# Ocamlopt     src/plugins/value/legacy/eval_annots.cmx
# Ocamlopt     src/plugins/value/engine/transfer_logic.cmx
# Ocamlopt     src/plugins/value/domains/cvalue/cvalue_domain.cmx
# /usr/bin/ld: cannot find -lgtksourceview-2.0
# collect2: error: ld returned 1 exit status
# Ocamlopt     src/plugins/value/domains/cvalue/cvalue_specification.cmx
# File "_none_", line 1:
# Error: Error while building custom runtime system
# make: *** [Makefile:1294: bin/viewer.byte] Error 2
# make: *** Waiting for unfinished jobs....

我最后的尝试是从源代码构建它，但是 make 失败并出现以下错误：

Ocamlc       src/plugins/server/jbuffer.cmo
File "src/plugins/server/jbuffer.ml", line 23, characters 12-26:
23 | type json = Yojson.Basic.t
                 ^^^^^^^^^^^^^^
Error: Unbound type constructor Yojson.Basic.t
make: *** [share/Makefile.generic:78: src/plugins/server/jbuffer.cmo] Error 2

我唯一剩下的解决方案是使用带有 debian 的 VM，但这对我来说真的很理想...... 有谁知道我能做什么？ 谢谢！

Answer 1

您的问题中有多个问题，我相信其中一些值得作为可能的错误或问题进行调查。我建议尝试使用 Frama-C 官方支持渠道之一：

• 在Frama-C Gitlab public repository 中创建问题；
• 或在Frama-C Github snapshot repository 中创建问题（目前已弃用，取而代之的是每天更新的 Gitlab 存储库）；
• 或者在 freenode.net 上的 IRC #frama-c 频道中尝试一些与 opam 相关的交互式支持（交互式支持对于与 opam 相关的安装问题通常更有效，特别是因为很难提前知道哪些信息可能有用） .

处理 GUI 中的“无效用户输入”错误

作为一般规则，当尝试在 GUI 中打开文件失败时，我建议使用文件名运行 Frama-C 的命令行版本。它的输出更加详细，并且可以指示文件是否存在解析问题（可能是由于缺少依赖项、非 C99 语法或配置问题）。

否则，GUI 中的“控制台”选项卡应包含详细的错误消息，然后您可以将其添加到此 SO 问题中，以防它们与理解您的问题相关。

非主要 Linux 发行版中的图形库问题

我在您的问题中看到的第二个问题是与-lgtksourceview-2.0 相关的错误。这意味着缺少图形界面的库依赖项之一。也许有办法修复它，但至少应该可以在编译之前识别错误，并更早地报告不兼容。 depext 不起作用的事实是不寻常的；也许它目前对 Manjaro 没有很好的支持，但值得研究。不幸的是，对于初次使用的用户来说，opam 有时处理起来很复杂，所以我知道这有点令人沮丧，并且可能需要比您想要的更多的时间。但是，如果您打算在一段合理的时间内使用 Frama-C 或其他 OCaml 包，则值得了解 opam 中的一些常见错误，因为它对于处理依赖关系非常有用。

手动编译时处理 OCaml 依赖问题

最后，Yojson 的问题可能是由于安装的包的版本。特别是，1.6.0 之前的版本没有Yojson.Basic.t 类型。 Frama-C 曾经支持 1.4.1，但最新版本至少需要 1.6.0。同样，提前发现不同软件包版本的所有可能问题并不明显，但报告它们允许我们包括检查以防止将来发生，或者至少给出更准确的错误消息。

通常 opam 会处理该部分，因此即使手动编译 Frama-C 也建议使用它，因为它有助于管理其依赖关系。

总体而言，opam depext 中依赖项的一些潜在问题似乎正在阻止整个链正常工作。您的报告确实包含很多有用的信息，但不是所有的细节，所以我相信交互式路线应该允许快速收敛到工作安装。