All geek questions in one place

Install Frama-C on Mac OS X

How to install the current version of Frama-C and its prerequisites on Mac computers?

I have a laptop running Mac OS X 10.6.8 and a desktop running Mac OS X 10.7.5 on which I can install the software. I also have access to the laboratory of machines running Mac OS X 10.8, which our technical support will install on if I ask beautifully.

I have a student who is interested in analyzing programs and needs something that we have a fighting chance to understand and add. I already knew about Frama-C, and a colleague at another university recommended it.

I previously tried installing Frama-C and failed unsuccessfully. A colleague commented that he had the same experience. Well, times are changing. So I visited the Frama-C website, was more impressed and sharper than ever, and more on that.

The download page of frama-c.com does not have links to any binary files for the current (Flourine 3) for any platform. A link to the installation instruction takes me to a page that says to download the auto-installer. What autoinstaller?

There are instructions for the old version of Mac OS X, but after them it does not work; loading one set of prerequisites in accordance with the instructions in which the following condition (gtksourceview) will not be installed.

Of course, I checked the old versions, and I see that there is a nitrogen version for Mac OS X Leopard, but "Please unzip the archive as root in /" asks me to do the impossible. I do not have a root account and will never be given (all machines belong to the university). it is entirely possible to install gcc and clang anywhere; Why does Frama-C want to be in /?

+4
source share
3 answers

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

+5
source

All the Frama-C binary packages they want to install in / (exactly, in / usr / local / Frama -C), because Frama-C uses GTK + and various GTK + -related libraries that were never intended to run from anything- or other than a fixed location. They load configuration files and resources from paths that were hard-coded at compile time. GCC and Clang are installed everywhere because they do not rely on GTK +. Like them, the Frama-C command line version can be ported through the environment variables listed here .

Please note that to use the binary package you will need only one symbolic link pointing from / usr / local / Frama -C to the place where you really extracted the files, if your administrator can provide this to you, Binary packages work only for one OS version X. For packages available on the official website, this version is usually 10.6 (Snow Leopard).

I stopped creating Frama-C binary packages for two reasons:

  • by removing features and supporting hardware configurations in each of the last two OS X releases, Apple has fragmented the OS X landscape in such a way that I don’t have time to solve. You mentioned 10.6, 10.7, and 10.8 in your question. I also have Mac computers running on each of 10.6, 10.7, and 10.8. All of them are incompatible (when trying to create a software package that includes a compiler).
  • Now I have much less time when I participate in the creation of a startup that offers Frama-C-based static analysis for interested industrial users.

This suggests that the Frama-C prototype Open-Source prototype continues to be developed and maintained and continues to be an excellent test bench for experiments. You can install Frama-C without root access on a Mac in two ways from what you have already tried:

  • Install only the command line version. Then the only dependency is the recent version of the OCaml compiler. Frama-C will detect that you do not have GTK libraries and will not try to use them. For the latest OCaml + the latest version of Frama-C, installation should take no more than 20 minutes.
  • Install the latest Linux distribution on the virtual machine. Use this distribution package manager to get all GTK + dependencies. If the distribution of the OCaml package is fairly recent, use it and then the lablgtk-2 package, otherwise compile OCaml and then lablgtk-2 from the source. Then compile Frama-C.

For Fluorine, the oldest version of OCaml is supported on 3.12.1.

+4
source

with 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
+1
source

Source: https://habr.com/ru/post/1495870/

More articles:


All Articles