Frama-C Installation

Currently (September 2014), Frama-C is installed most easily on UNIX-like operating systems, which include GNU/Linux, MacOS X, FreeBSD, OpenBSD. Ubuntu is one of many Linux distributions.

For installation on MSWindows, refer to the instructions in frama-c_windows.txt — Thanks to Yuriy!

Most Linux distributions come with (at least one) package manager; on MacOS X, use MacPorts. You need to know how to use your system's package manager.

(If your package manager provides Frama-C, check whether it is the latest version, namely Neon-20140301.)

Frama-C is implemented in OCaml; the easiest way to install the latest version of Frama-C should be using the OCaml package manager OPAM. (This is a separate package manager for packages implemented in OCaml. Once you use OPAM for OCaml packages, it is in general wise to not use your system package manager for these packages any more.)

• Use OCaml version 3.12.1, not version 4.
• If you want to install OPAM from source, you need to install OCaml first. Your package manager probably can do that for you.
• Follow the OPAM installation instructions (version 1.1.1 for now)
• Try:

  opam list -a
  

  This should produce a long list of available packages, with short descriptions. If it does not, you need to initialize OPAM — follow the instructions there carefully.
• Install Frama-C and essential prover support:

  opam install frama-c why
  

• Optionally install prover GUIs:

  opam install coqide altgr-ergo
  

Some distribution-specific hints:

On Ubuntu, before using Opam to install Frama-C etc.:

(and probably similarly on many other binary Linux distributions):

• For essential software development tools, you need:

  sudo apt-get install build-essential m4 autoconf libgmp-dev libgnomecanvas2-dev libgtk2.0-dev libgtksourceview2.0-dev
  

  (See e.g. here for more info.)
• Although many dynamically-linked libraries are already installed on your systems, binary Linux distributions normally don't install the associated header files. Those header files typically reside in packages with names ending in -dev.

  When OPAM fails to install OPAM package conf-XYZ, then you will likely need package XYZ-dev (or at least XYZ) from your Linux distribution.

On MacOS X:

• Get the Xcode development tools (and the X11 window system) from your MacOS X install medium, or from appropriate Apple sources
• Get the MacPorts package manager for free software for MacOS X