[Frama-c-discuss] Compiling Frama-C with Zarith under (Cygwin + ) Mingw
Dillon.Pariente at dassault-aviation.com
Thu Oct 20 10:56:40 CEST 2011
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
- GMP for Mingw (see
http://www.mingw.org/wiki/InstallationHOWTOforMinGW) ; => remove any
previous GMP installation coming with Cygwin (to avoid using
- 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:
-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!
# might not work properly, due to .so/.dll mismatch ... then try
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 ZARITH_INC="-I X:/path/to/ocaml_mingw/libraries/zarith/"
# and compile Frama-C (go to the Frama-C dir) ... as usual:
make && make install
For sure some of the (a bit tedious) instructions given above will be
once the Zarith feature will not be considered as experimental anymore!
More information about the Frama-c-discuss