User Tools

  • Logged in as: anonymous (anonymous)
  • Logout

Site Tools


mantis:frama-c:compiling_from_source

Compiling Frama-C from source

This page explains how to build Frama-C from source, for the platforms on which no binaries are available. If a binary is available at http://frama-c.com/download.html, we suggest you use it instead.

Compiling under Linux

If you are using Linux, your distribution may package Frama-C. This is currently the case for (at least) Ubuntu, Debian and Fedora.

If you want to compile a distribution more recent than the one packaged with your system, you will find detailed compilation instructions in the INSTALL file of the Frama-C tarballs.

Compiling under Windows (Cygwin + MinGW)

If you already know how to use OPAM, simply install the frama-c package. The instructions below are for users who have never used OPAM + Cygwin.

Although Frama-C is not officially supported on Windows (that is, the Frama-C team cannot guarantee that it will always work on Windows environments), it it possible to compile and use it. In case of errors, you can refer to StackOverflow questions tagged frama-c (or ask them yourself).

The recommended procedure is to use OPAM for MinGW OCaml:

  1. Install OCaml for Windows (the graphical installer should be fine). Note that newer releases of OCaml are not always backwards-compatible with Frama-C releases.
  2. Follow fdopen's instructions, in particular:
    • Install depext (opam install depext) and depext-cygwinports. This is necessary especially for the Frama-C GUI, which uses lablgtk.
    • Do not forget to update your PATH variable as indicated, or use ocaml-env.
  3. Install Frama-C dependencies:
    opam depext frama-c
  4. Install Frama-C itself:
    opam install frama-c

And it's done!

Note: By default, Cygwin defines the CPP variable in its environment. If you are using Frama-C 14 (Silicon) or older, append -C -I. to the value of that variable. For instance, by adding the following line to your .bashrc file:

export CPP="x86_64-w64-mingw32-cpp.exe -C -I."

The snippet above is for the 64-bit version.

You also need to systematically add -pp-annot to your command-line, otherwise annotations in source files may not be processed.

Obsolete procedures - should NOT be necessary (only presented for historical reasons)

An obsolete procedure using WODI is also presented but only for historical reasons. It is unlikely to work with recent lablgtk and Frama-C releases.

Note: the procedure below is not 100% robust, but it has been tested on a few different configurations. We recommend referring to the GitHub OPAM repository for MinGW or asking a question on StackOverflow if you have problems compiling it (e.g. if your Windows username contains spaces, this Cygwin FAQ referenced by fdopen indicates how to fix it).

Old procedure

1. Download (but do not run yet!) the Cygwin setup file to your Desktop.

  • Both 32-bit and 64-bit versions should work; we tested in particular the 32-bit version, which is the one used in the commands below.

2. Open a Command Prompt and run the command below to install Cygwin with necessary Frama-C dependencies.

  • The command below will use the downloaded Cygwin setup file.
  • You just have to keep clicking Next (using the default provided paths) and choose the Cygwin mirror of your preference. Then keep pressing Next and wait for the installation to finish.
%USERPROFILE%/Desktop/setup-x86.exe --root=C:/cygwin32 --local-package-dir C:/cygwin32/packages --no-startmenu --quiet-mode --packages=make,mingw64-i686-gcc-core,m4,patch,unzip,procmail,rsync,wget,diffutils,git,perl,curl,autoconf

3. Cygwin will create a Desktop shortcut. Open it and you will be presented a terminal. Use it to run the code below. Please note that this code downloads the OPAM for MinGW OCaml binaries from Dropbox.

  • You can copy the code below and paste it on the Cygwin terminal.
  • You can also click on frama-c-install-windows.sh to download the code. In that case, save it to your cygwin home directory (i.e. C:\cygwin32\home\<username>), and execute it on your Cygwin terminal: bash frama-c-install-windows.sh).
frama-c-install-windows.sh
#!/bin/bash -eu
 
# Download the OPAM 32-bit archive for MinGW (https://github.com/fdopen/opam-repository-mingw)
wget "https://dl.dropboxusercontent.com/s/eo4igttab8ipyle/opam32.tar.xz" -O opam32.tar.xz
 
# Uncompress and install OPAM
tar -xf 'opam32.tar.xz'
bash opam32/install.sh
 
# Use OPAM to install a 4.02.3 OCaml compiler
opam init mingw 'https://github.com/fdopen/opam-repository-mingw.git' --comp 4.02.3+mingw32 --switch 4.02.3+mingw32 --yes
 
# This variable is important for installing lablgtk
# If installing a 64-bit OCaml, replace "i686" with "x86_64"
export PATH=/usr/i686-w64-mingw32/sys-root/mingw/bin:$PATH
echo 'export PATH=/usr/i686-w64-mingw32/sys-root/mingw/bin:$PATH' >> .bashrc
 
# This is necessary for configuring OPAM
eval `opam config env`
echo 'eval `opam config env`' >> ~/.bashrc
 
# To apply a more modern-looking GTK theme
echo 'gtk-theme-name = "MS-Windows"' > ~/.gtkrc-2.0
 
# Install depext and depext-cygwinports, which will allow dependencies to be
# automatically installed
opam install depext depext-cygwinports --yes
 
# Install the latest available Frama-C and its dependencies using depext
OPAMYES=yes opam depext -i frama-c
 
echo "Done!"
echo "Do not forget to close and re-open your terminal to ensure that"
echo "environment variables are properly refreshed."

4. It's done! You can now run Frama-C from the command line (frama-c) or the GUI (frama-c-gui).

Old procedure based on WODI (GODI for Windows) + Cygwin + MinGW

Note: This procedure is now obsolete! Using OPAM should be easier (and also allows easier installation of optional Frama-C dependencies such as external solvers).

These steps were tested on a Sodium release with Cygwin 32 bits + WODI 32 bits, and then tested again on a Magnesium release with Cygwin 64 bits + WODI 64 bits. Similar combinations should work as well. They were tested on Windows 7 and on Windows 8.1.

These are thorough instructions to install Frama-C and its dependencies including the GUI. Some steps are not necessary if you do not need the GUI. These instructions are very detailed to help you troubleshoot if something unexpected happens.

The instructions below assume the 64-bit version in some commands; replace 64 with 32 when appropriate if using the 32-bit version.

  1. Install a native Windows OCaml compiler using Jonathan Protzenko's Ocaml on Windows installer. During OCaml installation, check the option to install Cygwin. It will put Cygwin's setup file in your Desktop.
    • Frama-C Sodium was tested using OCaml 4.02.1, 32-bit while Magnesium was tested using OCaml 4.02.3, 64-bit.
    • Note: The link to the 64-bit version includes OPAM, but we did not use it in our tests (issues with lablgtk prevented us from successfully running Frama-C's GUI).
  2. Install Cygwin (32-bit or 64-bit). You can use the setup file from Ocaml on Windows' installation. This will configure Cygwin's installation directory (e.g. C:\cygwin64) and a working mirror. This configuration will be later used to install required Cygwin packages.
    • Note that Cygwin's setup remember previous settings when run again; it works similarly to a graphical package manager on Debian systems, such as synaptic: you must run it again whenever you need to install or remove a package. After the first installation, you just have to click Next until the package selection screen is presented again.
  3. Using Cygwin's setup, install package mingw64-i686-gcc-core (for the 32-bit version) or mingw64-x86_64-gcc-core (for the 64-bit version).
    • Note that both use mingw64 in their name (this is not a typo).
    • Also note that these packages install cross-compilers, therefore there will be no gcc executable, but instead you'll have either i686-w64-mingw32-gcc on 32 bits or x86_64-w64-mingw32-gcc on 64 bits.
  4. Open a Cygwin terminal. Export the location of your Cygwin setup file under variable CYGSETUP_BIN, e.g. using this command:
    export CYGSETUP_BIN=/cygdrive/C/Users/Public/Desktop/cygwin-setup-x86_64.exe
    • (This step is not necessary per se, but it simplifies these instructions.)
    • Remember that this variable will not be saved across Cygwin sessions, so if you close and reopen your Cygwin terminal you'll need to export it again.
  5. Before installing WODI (for Frama-C dependencies), you'll need to install a few additional Cygwin packages. Using the CYGSETUP_BIN variable defined previously, you can run:
    "$CYGSETUP_BIN" --quiet-mode --no-desktop --no-startmenu --packages=dos2unix,diffutils,cpio,make,patch,rlwrap
    • If you have issues or need more information, follow the instructions in WODI's page.
  6. Install WODI by downloading and uncompressing its tar.xz archives.
    • WODI has been discontinued, but its installer and a tar.xz containing its binary packages are still available on its website.
    • The 32-bit version has been tested with Frama-C Sodium and the 64-bit version has been tested with Frama-C Magnesium.
    • Quick installation: uncompress WODI (tar xvf wodi64.tar.xz), run cd wodi64 and then ./install.sh. This should copy WODI's files to /opt/wodi64.
    • Run tar xvf packages64.tar.xz and put its files (all files inside the directory, without the directory name itself) into your Cygwin's /opt/wodi64/var/cache/godi directory (e.g. C:\cygwin64\opt\wodi64\var\cache\godi). This can be done by running:
      mv packages64/* /opt/wodi64/var/cache/godi/
      • Note that installing WODI in another directory may require patching configuration files, otherwise it may not recognize the installed packages.
  7. Close the terminal and open a new Cygwin terminal to refresh the environment variables. Test if WODI was properly installed, by running a command such as godi_list.
    • WODI may complain about spaces in your PATH variable (make sure they do not occur in Cygwin/GODI/OCaml-related directories, or things may not work), but it should display a huge list of packages (with a few of them installed).
  8. Install packages zarith, lablgtk, and optionally ocamlgraph:
    godi_add godi-zarith godi-lablgtk2 godi-ocamlgraph
    • This command may take a while and will not output anything if successful, other than a possible warning about spaces in your PATH variable.
  9. Download Frama-C's source release (tested with Sodium and Magnesium)
  10. Using the Cygwin shell, uncompress Frama-C's sources, cd into it, and run configure as follows:
    CC=x86_64-w64-mingw32-gcc configure --prefix="C:/path/to/final/framac"
    • Where path/to/final/framac is the directory where you want Frama-C to be installed.
    • Important: this path must be written using a Windows-based path and not a Cygwin-based one such as '/home/user/framac'. Also, use forward slashes (/) instead of backslashes, otherwise Frama-C will install but not run properly.
    • Use CC=i686-w64-mingw32-gcc instead if you're installing the 32-bit version.
    • Here's an example command-line to install Frama-C to a local build directory:
      CC=x86_64-w64-mingw32-gcc ./configure --prefix="$(cygpath -a -m $PWD)"/build
  11. Check that the ./configure script found the required dependencies (e.g. for the GUI). The GUI may be partially disabled if dot is not installed, but otherwise it should have detected lablgtk correctly.
    • If you want the GUI and the callgraph to be fully enabled, install Cygwin package graphviz.
  12. (Magnesium only) Frama-C Magnesium requires a patch to the Makefile, otherwise the following error may occur:
    [...]
    Generating .depend /bin/sh:
    /opt/wodi64/bin/ocamldep.opt: Argument list too long
    • This is the patch to be applied: Makefile-ocamldep-argument-too-long.patch
    • Download the patch file to your Frama-C source directory, and apply it using e.g.:
      patch -i makefile-ocamldep-argument-too-long.patch
  13. Run make using the special value for variable FRAMAC_TOP_SRCDIR below:
    make FRAMAC_TOP_SRCDIR="$(cygpath -a -m $PWD)"
    • This will fix the path during execution of the Makefile, using a Windows-based absolute path instead of a Cygwin-based one. Without this fix, compilation will fail after some time (when compiling plugin files).
    • Note that the first time make runs, it may emit some warnings about missing files such as the ones below, but this is normal and should not affect compilation:
      C:/cygwin64/home/user/frama-c-Magnesium-20151002/share/Makefile.dynamic:195: share/Makefile.kernel: No such file or directory
      C:/cygwin64/home/user/frama-c-Magnesium-20151002/share/Makefile.dynamic:195: share/Makefile.kernel: No such file or directory
      C:/cygwin64/home/user/frama-c-Magnesium-20151002/share/Makefile.dynamic:195: share/Makefile.kernel: No such file or directory
      C:/cygwin64/home/user/frama-c-Magnesium-20151002/share/Makefile.dynamic:195: share/Makefile.kernel: No such file or directory
      C:/cygwin64/home/user/frama-c-Magnesium-20151002/share/Makefile.dynamic:195: share/Makefile.kernel: No such file or directory
      Makefile:2434: .depend: No such file or directory
  14. Get a coffee while waiting for Frama-C to compile, it may take a while.
  15. Run make install. Your Frama-C is now ready to be used!
    • If you installed Frama-C in a directory which is not in the PATH, remember to prefix it with /path/to/installed_framac/bin/.
  16. Try parsing a simple program, e.g. frama-c file.c or frama-c-gui file.c, to ensure that all necessary paths are correct (such as __fc_builtin_for_normalization.i).
    • You can also try one of Frama-C's tests, e.g. frama-c-gui tests/idct/*.c. Note that the tests/idct contains a single test split in two C files, but most other test directories contain unit tests which should be run individually. Also note that several tests do not constitute valid C programs.
Note

There is a Windows-specific issue in Frama-C Sodium/Magnesium that prevents Windows absolute paths with backslashes from being correctly parsed. In the command-line, you can use forward slashes (frama-c 'C:/Temp/file.c') or double backslashes (frama-c 'C:\\Temp\\file.c'), but in the GUI you cannot load files using absolute paths. There is however a patch in the OPAM-MinGW version of Magnesium that fixes this issue.

  • GNU make version >= 3.81
  • Objective Caml >= 4.02.3;
  • Gtk (>= 2.4)
  • GtkSourceView 2.x
  • GnomeCanvas 2.x
  • LablGtk >= 2.18.3

Sources:

Older versions

Nitrogen

Compiling under Cygwin with Mingw, with Zarith

The following is taken directly from Dillon Pariente's informative message http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-October/002837.html .

You might like to also have a look at http://blog.frama-c.com/index.php?post/2011/10/09/Zarith and http://blog.frama-c.com/index.php?post/2011/10/17/Features-in-Nitrogen-1 to check the advantages you can draw from using Zarith.

The description for the Zarith library reads as follows:

“The Zarith library implements arithmetic and logical operations over arbitrary-precision integers. It uses GMP to efficiently implement arithmetic over big integers. Small integers are represented as Caml unboxed integers, for speed and space economy.”

It is available from http://forge.ocamlcore.org/projects/zarith/ and expected to improve performances up 50% in the best cases.

What follow are some informal hints for the ones interested in using this new experimental Zarith feature under Mingw (or Cygwin+Mingw).

Requirements

Prior to reproducing the steps below, check that you have the following

svn checkout svn://scm.ocamlcore.org/svn/zarith/trunk) 
Zarith's configuration and compilation

Now, configure and compile Zarith (under the zarith installation dir), following the command lines below:

export FLEXLINKFLAGS="-LX:/path/to/mingw/libraries"

CPPFLAGS="-IX:/path/to/mingw/includes -IX:/path/to/ocaml_mingw_port/includes -D__MINGW32__ -mno-cygwin" ./configure --installdir X:/path/to/ocaml_mingw_port/libraries

make clean && make depend && make
make test && ./test
# to check whether zarith compilation is OK!

make install

If the last command does not work properly, due to .so/.dll mismatch … then try instead:

ocamlfind install -destdir X:/path/to/ocaml_mingw/libraries zarith META zarith.cma libzarith.a z.mli q.mli big_int_Z.mli z.cmi q.cmi big_int_Z.cmi zarith.a zarith.cmxa zarith.cmxs dllzarith.dll
Compiling Frama-C with Zarith support

Now, you can define some required environment variables:

export HAS_ZARITH=yes
export ZARITH_INC="-I X:/path/to/ocaml_mingw/libraries/zarith/"

And compile Frama-C (go to the Frama-C dir) … as usual:

./configure ...
make && make install

The instructions below refer to previous versions of Frama-C, and may not apply to the most current one. If you succeed in compiling a more recent version than the one for which the instructions were originally written, do not hesitate to update this page.

Beryllium installation

Compiling Beryllium for Mac OS X

To compile Frama-C for Mac OS X Leopard yourself, see this message.

Compiling Beryllium for FreeBSD

To compile Frama-C on FreeBSD, use env MAKE=gmake bash ./configure CFLAGS=”-I/usr/local/include” LDFLAGS=”-L/usr/local/lib” && gmake

Compiling the Jessie plugin coming with Why 2.22 under Windows?

  1. Install the Windows binary 20090902 Beryllium Frama-C version
  2. Set the following environment variables (using the Windows Control Panel):
    • prepend C:\Frama-C\bin to PATH
    • set OCAMLLIB to C:\Frama-C\lib
    • set CAML_LD_LIBRARY_PATH to C:\Frama-C\lib\stublibs
      Replace C:\Frama-C by your installation path if you customized it.
  3. Install a Cygwin version (1.7 beta has been verified to work) with at least the gcc-mingw and autoconf packages
  4. If C:\Cygwin\bin\gcc.exe is a symbolic link, remove it and replace it by its full expansion e.g. gcc-3.exe under Cygwin 1.7 beta.
  5. Download the source tar.gz of Why 2.22
  6. untar it in your cygwin home directory
  7. configure it with ./configure –prefix C:/Frama-C (forward slash must be used!)
  8. compile it with make
  9. install it with make FRAMAC_LIBDIR=“C:\\\Frama-C\\\lib\\\frama-c” install (triple backward slashes must be used!)
  10. then proceed to the installation of provers
mantis/frama-c/compiling_from_source.txt · Last modified: 2017/03/15 18:18 by maroneze