在 Mac OS X 上安装 Frama-C

Question

如何在 Mac 上安装当前的 Frama-C 版本及其先决条件？

我有一台运行 Mac OS X 10.6.8 的笔记本电脑和一台运行 Mac OS X 10.7.5 的台式机 我可以在上面安装软件。我还可以使用机器实验室 运行 Mac OS X 10.8，我们的技术支持人员将在其上安装东西 如果我问得好。

我有一个学生对程序分析感兴趣并且需要一些东西 我们有机会理解和补充。我已经 知道 Frama-C，另一所大学的同事推荐了它。

我之前曾尝试安装 Frama-C，但惨遭失败。同事 评论说他也有同样的经历。嗯，时代变了。所以我参观了 Frama-C 网站比以往任何时候都更令人印象深刻和渴望拥有它，并且 开始吧。

frama-c.com 下载页面没有指向任何二进制文件的链接 适用于任何平台的当前（Flourine 3）版本。安装链接 指令将我带到一个说下载自动安装程序的页面。 什么自动安装程序？

有旧版 Mac OS X 的说明，但请遵循这些说明 没用；按照指示加载一组先决条件产生了 说明下一个先决条件 (gtksourceview) 不会安装的位置。

当然，我检查了旧版本，发现有一个 Nitrogen Mac OS X Leopard 的版本，但“请在 / 中以 root 身份解压存档” 要求我完成不可能的事情。我没有 root 帐户，我会 永远不要给一个（机器都属于大学）。这是 完全可以在任何你喜欢的地方安装 gcc 和 clang；为什么 Frama-C 想在 / 中吗？

Answer 1

除了 Pascal 的回答，您还可以查看 opam，它是 OCaml 应用程序的源包管理器。它似乎可以在 MacOS X 上运行，并且有 Frama-C 的 Oxygen 和 Fluorine 软件包。

Answer 2

所有 Frama-C 二进制软件包都希望安装在 / 中（准确地说，在 /usr/local/Frama-C 中），因为 Frama-C 使用 GTK+ 和各种与 GTK+ 相关的库，这些库从未设计为从除固定位置。它们从在编译时硬编码的路径中加载配置文件和资源。 GCC 和 Clang 可以安装在任何地方，因为它们不依赖 GTK+。和他们一样，Frama-C 的命令行版本可以通过here 列出的各种环境变量重新定位。

请注意，要利用二进制包，您只需要一个从 /usr/local/Frama-C 指向您真正提取文件的位置的符号链接，如果您的管理员可以授予您.二进制包仅适用于一个 OS X 版本。对于官网提供的包，这个版本通常是10.6（雪豹）。

---

我已经停止制作 Frama-C 二进制包有两个原因：

1. 通过在最后两个 OS X 版本中删除功能和对硬件配置的支持，Apple 以我没有时间处理的方式分割了 OS X 格局。您在问题中提到了 10.6、10.7 和 10.8。我也有运行 10.6、10.7 和 10.8 的 Mac。它们都是不兼容的（在尝试构建包含编译器的软件包时）。
2. 现在我参与创建一家为感兴趣的工业用户提供基于 Frama-C 的静态分析的初创公司的可用时间要少得多。

也就是说，开源高级研究原型 Frama-C 继续得到开发和维护，并且仍然是一个很好的试验平台。您可以通过两种方式在 Mac 上安装 Frama-C 而无需 root 访问权限从你已经尝试过的：

1. 仅安装命令行版本。那么唯一的依赖就是最新版本的 OCaml 编译器。 Frama-C 的配置将检测到您没有 GTK 库并且不会尝试使用它们。对于最新的 OCaml + 最新的 Frama-C，安装最多需要 20 分钟。
2. 在虚拟机中安装最新的 Linux 发行版。使用该发行版的包管理器来获取所有 GTK+ 依赖项。如果发行版的 OCaml 包足够新，请使用它，然后使用 lablgtk-2 包，否则，从源代码编译 OCaml，然后编译 lablgtk-2。然后编译 Frama-C。

对于 Fluorine，支持的最旧 OCaml 版本是 3.12.1。

Answer 3

使用 macports：

export PKG_CONFIG_PATH=/opt/local/lib/pkgconfig
sudo port install opam
opam init
  Y
eval `opam config env`
sudo port install gtksourceview2 lablgtk2 ocaml-ocamlgraph
opam install frama-c