SYSTEM WARNING: 'session_name(): Cannot change session name when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 231
SYSTEM WARNING: 'session_set_cookie_params(): Cannot change session cookie parameters when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 232
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.
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.
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:
opam install depext) and depext-cygwinports. This is necessary especially for the Frama-C GUI, which uses lablgtk.
opam depext frama-c
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
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.
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).
1. Download (but do not run yet!) the Cygwin setup file to your Desktop.
2. Open a Command Prompt and run the command below to install Cygwin with necessary Frama-C dependencies.
%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.
frama-c-install-windows.shto 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:
#!/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 (
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
32 when appropriate if using the 32-bit version.
C:\cygwin64) and a working mirror. This configuration will be later used to install required Cygwin packages.
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.
mingw64-i686-gcc-core(for the 32-bit version) or
mingw64-x86_64-gcc-core(for the 64-bit version).
mingw64in their name (this is not a typo).
gccexecutable, but instead you'll have either
i686-w64-mingw32-gccon 32 bits or
x86_64-w64-mingw32-gccon 64 bits.
CYGSETUP_BIN, e.g. using this command:
CYGSETUP_BINvariable defined previously, you can run:
"$CYGSETUP_BIN" --quiet-mode --no-desktop --no-startmenu --packages=dos2unix,diffutils,cpio,make,patch,rlwrap
tar xvf wodi64.tar.xz), run
cd wodi64and then
./install.sh. This should copy WODI's files to
tar xvf packages64.tar.xzand put its files (all files inside the directory, without the directory name itself) into your Cygwin's
C:\cygwin64\opt\wodi64\var\cache\godi). This can be done by running:
mv packages64/* /opt/wodi64/var/cache/godi/
PATHvariable (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).
godi_add godi-zarith godi-lablgtk2 godi-ocamlgraph
cdinto it, and run configure as follows:
CC=x86_64-w64-mingw32-gcc configure --prefix="C:/path/to/final/framac"
path/to/final/framacis the directory where you want Frama-C to be installed.
/) instead of backslashes, otherwise Frama-C will install but not run properly.
CC=i686-w64-mingw32-gccinstead if you're installing the 32-bit version.
CC=x86_64-w64-mingw32-gcc ./configure --prefix="$(cygpath -a -m $PWD)"/build
./configurescript found the required dependencies (e.g. for the GUI). The GUI may be partially disabled if
dotis not installed, but otherwise it should have detected lablgtk correctly.
Makefile, otherwise the following error may occur:
[...] Generating .depend /bin/sh: /opt/wodi64/bin/ocamldep.opt: Argument list too long
patch -i makefile-ocamldep-argument-too-long.patch
makeusing the special value for variable
make FRAMAC_TOP_SRCDIR="$(cygpath -a -m $PWD)"
makeruns, 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
make install. Your Frama-C is now ready to be used!
frama-c-gui file.c, to ensure that all necessary paths are correct (such as
frama-c-gui tests/idct/*.c. Note that the
tests/idctcontains 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.
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.
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).
Prior to reproducing the steps below, check that you have the following
svn checkout svn://scm.ocamlcore.org/svn/zarith/trunk)
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
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.
To compile Frama-C for Mac OS X Leopard yourself, see this message.
To compile Frama-C on FreeBSD, use
env MAKE=gmake bash ./configure CFLAGS=“-I/usr/local/include” LDFLAGS=“-L/usr/local/lib” && gmake
C:\Frama-Cby your installation path if you customized it.
C:\Cygwin\bin\gcc.exeis a symbolic link, remove it and replace it by its full expansion e.g.
gcc-3.exeunder Cygwin 1.7 beta.
./configure –prefix C:/Frama-C(forward slash must be used!)
make FRAMAC_LIBDIR=“C:\\\Frama-C\\\lib\\\frama-c” install(triple backward slashes must be used!)