4

如何在 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）不会安装的状态。

当然，我检查了较旧的版本，发现有 Mac OS X Leopard 的 Nitrogen 版本，但是“请将存档解压缩为 /​​ 中的根目录”要求我执行不可能的操作。我没有 root 帐户，也永远不会得到一个（机器都属于大学）。完全可以在任何你喜欢的地方安装 gcc 和 clang；为什么 Frama-C 想要在 / 中？

4

3 回答 3

5

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

于 2013-08-08T12:56:56.953 回答
4

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

请注意，要利用二进制包，您只需要一个从 /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。

于 2013-08-08T06:33:41.293 回答
1

使用 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
于 2014-04-12T13:59:08.260 回答