Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Compiling Frama-C with Zarith under (Cygwin + ) Mingw

  • Subject: [Frama-c-discuss] Compiling Frama-C with Zarith under (Cygwin + ) Mingw
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
  • Date: Thu, 20 Oct 2011 10:56:40 +0200
Hello,

Many thanks to the Frama-C team for the new Nitrogen release.

In another mailing-list, the Frama-C developers exposed that it was 
possible to link Frama-C with the Zarith library (so, requiring to 
recompile Frama-C from the source distribution).

Zarith is available at http://forge.ocamlcore.org/projects/zarith/
and is defined 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 expected to improve perfos in some cases from 30% to 50%.

What follow are some informal hints for the ones interested in using 
this new experimental Zarith feature under Mingw (or Cygwin+Mingw). 
Thanks in advance to our great experts Pascal and Boris to 
correct/complete these if needed.

Some of the main requirements I used:
- ocaml port mingw     3.12.0 or higher
- flexlink (from http://alain.frisch.fr/flexdll.html)
- Zarith lib (brought by: svn checkout 
svn://scm.ocamlcore.org/svn/zarith/trunk)
- GMP for Mingw (see 
http://www.mingw.org/wiki/InstallationHOWTOforMinGW) ; => remove any 
previous GMP installation coming with Cygwin (to avoid using
cygwin1.dll!!)
- and all other requirements expressed into the Frama-C's INSTALL file.

Then configure and compile Zarith (under the zarith installation dir), 
with 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
# might 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

# then define some required env-vars:

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

For sure some of the (a bit tedious) instructions given above will be
soon improved, 
once the Zarith feature will not be considered as experimental anymore!

HTH!

Best,
Dillon