Frama-C：在 Cygwin / Windows 8.1 上编译

Question

对于那些在 windows 上编译 C 的人来说一个简单的问题！

我想在 Windows 8 上使用最新版本的 Frama-C C 静态分析器及其 GUI。据我所知，具有 Windows 安装程序的最新版本是 Boron，大约是 3-4岁。所以看起来我需要自己编译它（版本 Fluorine 3）。但是，我在最初的几个步骤中磕磕绊绊。

Frama-C Fluorine 3 的快速启动编译说明是here。

• 第 1 步：安装 OCaml。我已经从here安装了windows版本。

• 步骤 1b：我相信步骤 1 安装了 Gtk 等等。

• 步骤 2b：运行：

  ./configure --prefix C:/windows/path/with/direct/slash && make && make install

关于这些说明的 4 件事让我感到困惑：

1. 这是指哪个configure 文件？如果我打开 Cygwin 终端，它会让我进入用户的主目录，如果我运行 ./configure，它会说没有这样的文件或目录。我认为它是指引用源中的配置文件之一，但有超过 10 个。

2. C:/windows/path/with/direct/slash 到底是什么意思？请问有人可以给我一个很好的解释的真实例子吗？

3. 我应该在哪个目录中运行上述命令（步骤 2b）？

4. 我应该将提取的 Frama-C 源代码分发放在哪个目录中？ （我应该只从存档中提取 src 目录，还是需要所有内容？）

我要做的就是按照他们主页链接的“Short example”，使用最新版本，在 Windows 8.1 上，我需要一个“绝对傻瓜”指南来这样做！

非常感谢

Answer 1

我遇到了您的问题，因为我也对“with/direct/slash”指令感到困惑。至少我可以帮助您解决其他问题：

1. 按照惯例，它始终是 tarball 根目录中的配置文件。因此，解压缩 tar.gz 文件，然后 cd 进入创建并从那里运行 ./configure 的目录。

2. --prefix 定义了安装路径，所以我假设这个选项应该把可执行文件放在某个可以从 Windows 轻松访问的目录中（例如 Program Files 目录）。我不确定“直接斜杠”位是什么。通常，Cygwin 的根目录实际上是 C: 驱动器上的某个目录（例如 C:\cygwin），因此要访问文件层次结构的其余部分，通常在 Cygwin 根目录中有一个名为“cygdrive”的映射挂载。这样，您可以使用“/cygdrive/c/path/to/windows/directory”之类的内容从 Cygwin 中导航到广泛的层次结构。在 Cygwin 中使用“C:/”有点奇怪。对于它的价值，我只接受默认值（无 --prefix 标志）或在 Cygwin 层次结构中指定一些东西，如 '/usr/local/bin' 并从那里运行它。

3. 从您指定的“--prefix”目录中，因为这是可执行文件所在的位置。如果将其保留为默认值之一，则可以从任何地方运行可执行文件，因为它将位于 PATH 中的某个位置。

4. 将整个文件解压缩到主文件夹中的某个工作目录中。一旦你安装了它（这是 './configure && make && make install' 所做的），你可以扔掉提取的档案。

Answer 2

Updated instructions about compiling Frama-C on Windows 可在 Frama-C wiki 上找到，并在 Windows 7 和 Windows 8.1 上进行了测试。

这些说明不受官方支持，但它们应该可以帮助用户使用 OPAM（OCaml 包管理器）编译和安装 Frama-C。

此外，由于最近的 Windows 版本之间的过程没有显着差异，因此this question 的一些答案也可能适用于您的情况。

Answer 3

在 Windows 10 中，按照以下说明成功安装了 frama-c：

1. 在 Windows 10 中启用 WSL

https://docs.microsoft.com/en-us/windows/wsl/install-win10

Ubuntu 现在应该在 Windows 菜单中可用。运行它并按照说明创建用户。

1. 为了安装 opam，

   1. sudo add-apt-repository -y ppa:snwh/ppa
   2. sudo apt update
   3. sudo apt upgrade
   4. sudo apt install make m4 gcc opam

2. 可以使用以下方法设置 opam：

   1. opam init --disable-sandboxing -c 4.07.0 --shell-setup

      如果存在 opam 开关错误，则运行以下命令：

      opam switch create 4.07.0
      

      这将下载并安装 ocaml 编译器 4.07.0 版本。

   2. eval $(opam env)

   3. opam install -y depext

3. 要安装 Frama-C，请运行以下命令：

   1. opam depext --install -y lablgtk3 lablgtk3-sourceview3
   2. opam depext conf-gnomecanvas
   3. opam depext conf-gtksourceview
   4. opam depext --install -y frama-c

   这应该处理大约 70 个文件，安装需要一些时间。

   5. eval $(opam config env)

   再次重启Ubuntu，如果出现“command not found”问题，则再次执行命令“eval $(opam config env)”，使用frama-c。

4. 安装 Frama-c 21.1 后，进行测试：

   1. which frama-c
   2. which frama-c-gui

   如果两个命令都显示正确的安装目录，那么它们将成功执行。

5. frama-c-gui 安装后，由于 WSL 不支持 GUI，所以我使用了 mobaXterm。

   1. 安装 MobaXterm。 Xserver 默认随 MobaXterm 提供。
   2. 当您启动 MobaXterm 时，Xserver 图标出现在右上角。点击开始。
   3. Xserver 启动后，将鼠标悬停在图标上以查看 GUI 显示的 IP 地址。示例将显示：“172.19.64.1:0.0”。请注意这一点。
   4. 在 Ubuntu 中，export DISPLAY="172.19.64.1:0.0"
   5. 然后启动 frama-c-gui。它将使用 Xserver GUI 打开。

如果使用安装在 virtual box 中的 Virtual Box 和 Linux 发行版，请按照步骤 2 到 5 进行安装。为成功安装至少分配 20 GB 到虚拟盒。只有在分配了足够的磁盘空间时才会安装 frama-c-gui。