install Frama-C on Mac OS X

Question

How do I install a current Frama-C release and its prerequisites on Macs?

I have a laptop running Mac OS X 10.6.8 and a desktop running Mac OS X 10.7.5 which I can install software on. I also have access to a lab of machines running Mac OS X 10.8 which our technical support people will install stuff on if I ask nicely.

I have a student who is interested in program analysis and needs something that we have a fighting chance of understanding and adding to. I was already aware of Frama-C, and a colleague at another university recommended it.

I had previously tried to install Frama-C and failed miserably. The colleague commented that he'd had the same experience. Well, times change. So I visited the Frama-C web site, was more impressed and keener to have it than ever, and set about it.

The frama-c.com download page doesn't have links to any binaries for the current (Flourine 3) release for any platform. The link to installation instruction takes me to a page that says to download the auto-installer. What auto-installer?

There are instructions for an old version of Mac OS X, but following them didn't work; loading one set of prerequisites as instructed produced a state where the next prerequisite (gtksourceview) would not install.

Of course I checked the older releases, and I see that there's a Nitrogen version for Mac OS X Leopard, but "Please untar the archive as root in /" asks me to perform the impossible. I don't have a root account and will never be given one (the machines all belong to the university). It is perfectly possible to install gcc and clang anywhere you like; why does Frama-C want to be in /?

Answer 1

In addition to Pascal's answer, you can also have a look to opam, which is a source package manager for OCaml applications. It appears to run on MacOS X, and there are packages for Frama-C's Oxygen and Fluorine.

Answer 2

All Frama-C binary packages want to install in / (precisely, in /usr/local/Frama-C) because Frama-C uses GTK+ and various GTK+-related libraries that were never designed to run from anything other than a fixed location. They load configuration files and resources from paths that have been hard-coded at compile-time. GCC and Clang install anywhere because they don't rely on GTK+. Like them, the command-line version of Frama-C can be relocated through various environment variables listed here.

Note that to take advantage of a binary package, you would only need one symbolic link pointing from /usr/local/Frama-C to the place where you really extracted the files, if your administrator(s) can grant you that. Binary packages only work for one OS X version. For packages available from the official website, this version is usually 10.6 (Snow Leopard).

---

I have ceased making Frama-C binary packages for two reasons:

1. by removing features and support for hardware configurations in each of the last two OS X releases, Apple has fragmented the OS X landscape in a way I don't have the time to deal with. You mention 10.6, 10.7 and 10.8 in your question. I also have Macs running each of 10.6, 10.7 and 10.8. They are all incompatible (when trying to build a software package that includes a compiler).
2. I have much less time available now that I am participating in the creation of a start-up that offers Frama-C-based static analysis to interested industrial users.

This said, Frama-C the Open-Source advanced research prototype continues to be developed and maintained, and continues to be a great testbed to experiment in. You can install Frama-C without root access on a Mac in two ways apart from what you have already tried:

1. Install only the command-line version. Then the only dependency is a recent version of the OCaml compiler. Frama-C's configure will detect that you do not have the GTK libraries and will not try to use them. Installation should take 20 minutes at most for a recent OCaml + the latest Frama-C.
2. Install a recent Linux distribution in a virtual machine. Use that distribution's package manager to obtain all the GTK+ dependencies. If the distribution's OCaml package is recent enough, use that and then the lablgtk-2 package, otherwise, compile OCaml and then lablgtk-2 from source. Then compile Frama-C.

For Fluorine, the oldest supported OCaml version is 3.12.1.