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] RE : New Why Release on Mac OS Snow Leopard

Hello,

> I installed the new Why version, 
> but it is incompatible with the Frama-C release
> for Mac OS Snow Leopard that is available on the web page.

Well, it is complicated.

The intention with the binary Mac OS X distribution
was to make it possible to compile and install new plug-ins,
such as Jessie. The complete OCaml environment that was used
for compiling Frama-C is provided for this purpose, and takes
40 or so of the compressed 100 MB of the binary distribution.

If you were on Leopard, it would work perfectly: just
set your PATH variable so that the provided ocaml is used
and you're set 
(it is in /usr/local/Frama-C_Be/ocaml-3.11.1/bin in the Intel
distribution).

Unfortunately, although it is possible with a little hacking
to compile a 32 bit OCaml compiler that supports
dynlink on Snow Leopard, the 32-bit OCaml compiler
obtained by compiling OCaml on Leopard doesn't support
dynlink. That Leopard OCaml passes the wrong options
to the linker or something.

That leaves you the possibility to compile, with the
OCaml compiler provided in the binary distribution, 
a statically linked version of the new Jessie plug-in.
This should work, although I did not quite have the time
to test it yet.

I expect that the procedure is, after having set your PATH
to use /usr/local/Frama-C_Be/ocaml-3.11.1/bin/ocaml,
to type "make static" in the Jessie Frama-C plug-in's
directory, which is a sub-directory of the Why source
distribution.

You can compile Why itself with whatever compiler you like.
Keep the version you have already obtained, it poses no
compatibility problem because it is a separate binary.

Good luck,

Pascal