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] Oxygen on Mac OS X Mountain Lion


  • Subject: [Frama-c-discuss] Oxygen on Mac OS X Mountain Lion
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
  • Date: Sat, 6 Oct 2012 06:24:59 +0000
  • In-reply-to: <CABbVA-AX-=oLGn_Zar-KfdY2Z3MkECUAyMj25PwOcyHEactY-w@mail.gmail.com>
  • References: <250FB41C2DF1D14FA9D5971909DE405629278034@exdb00.first.fraunhofer.de> <CABbVA-AX-=oLGn_Zar-KfdY2Z3MkECUAyMj25PwOcyHEactY-w@mail.gmail.com>

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