Frama-C-discuss mailing list archives

jens.gerlach at first.fraunhofer.de (Jens Gerlach) · Sat, 6 Oct 2012 06:24:59 +0000

Hello Boris,

thank you for your follow-up.
In the meantime , I have made considerably progress installing Frama-C Oxygen on
OS X in general and Mountain Lion (OS X 10.8.2) in particular.
Despite some challenges I found Oxygen much easier to install under OS X
than previous versions of Frama-C! 

Here is how I made it work:
I installed macports and and from there the following packages:

	sudo port install gtksourceview2
	sudo port install lablgtk2 +gtksourceview2
		(this one was tricky because macports mentions only a variant +gtksourceview (without the "2"))
	sudo ocaml-zarith ocaml-ocamlgraph
		(thanks for the hint to install zarith, Boris!)
	sudo port install graphviz
	sudo port install coq
	sudo port install djvulibre
		(I am not sure I really needed this package but I remembered that Pascal Cuoq
			had mention these fonts earlier)

Then I installed the alt-ergo binary under /opt/local/bin.
(I took the binary because configuring alt-ergo with prefix "/opt/local" would not find ocamlgraph
and I was too impatient to examine this more closely.)

Finally, I configured the Frama-C sources with prefix "/opt/local".
"make" and "make install" worked fine.

NOTE 1:
Under Mountain Lion the installed binaries "frama-c-gui" and "frama-c"
DO NOT WORK (segmentation fault). This is probably related to the bug of ocaml
under Mountain Lion mentioned here:
	http://stackoverflow.com/questions/11762774/why-do-ocaml-binaries-crash-on-mac-os-x-10-8-mountain-lion
The solution is to use the executables "frama-c-gui.byte" and "frama-c.byte".
Under Lion (OS X 10.7) and Snow Leopard (OS X 10.6) the other binaries do work.

NOTE 2:
So far I have only tested Frama-C/WP.

Regards

Jens

On 05.10.2012, at 13:56, Boris Yakobowski <boris at yakobowski.org> wrote:

> Hi Jens
> 
> Disclaimer : I'm not a mac expert at all (quite the contrary in fact),
> but not many people currently use one here.
> 
> On Wed, Sep 26, 2012 at 8:47 AM, Jens Gerlach
> <jens.gerlach at first.fraunhofer.de> wrote:
>> configure: gui: no, /opt/local/lib/ocaml/site-lib/lablgtk2/lablgtksourceview2.cmxa missing
>> 
>> but there is
>>     /opt/local/lib/ocaml/site-lib/lablgtk2/lablgtksourceview.cmxa
>> available (without the the final "2").
> 
> I'm afraid this might the binding for labgtksourceview1. If so, the
> compilation of the GUI will fail later. Did you compile Lablgtk
> yourself, or did you get a package?
> 
>> Generating   src/lib/my_bigint.ml
>> sed: RE error: illegal byte sequence
>> make: *** [src/lib/my_bigint.ml] Error 1
> 
> According to someone more knowledgeable than me, this is the result of
> a not-so intelligent change from Apple in its sed implementation.
> Google tells us that the encoding of the file on which sed is applied
> must correspond to you C locale (see eg.
> https://trac.macports.org/ticket/35421). A few possibilities :
> - reencode src/lib/my_bigint.ml.bigint in utf-8 (assuming you use this locale)
> - change your C locale to iso8859-1 (untested, should work)
> - install Zarith :-)
> 
> A last word of warning: the C linker in Mountain Lion do not cooperate
> very well with the current OCaml compilers, so it is not clear that
> compilation will succeed afterwards anyway.
> 
> HTH,
> 
> -- 
> Boris
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-- 

Dr.-Ing. Jens Gerlach 
Quality for Embedded Systems (QUEST)
Phone +49 (0)30 6392 1841, jens.gerlach at first.fraunhofer.de
Fraunhofer Institute for Open Communication Systems
Fraunhofer FOKUS, Kekulestrasse 7, D 12489 Berlin, Germany

Frama-C-discuss mailing list archives

[Frama-c-discuss] Oxygen on Mac OS X Mountain Lion