--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on April 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] problem with installation of Frama-C Beryllium (2) for Mac OS X 10.5.8



Thanks Pascal for your help.

You guessed right. The first error was because of the tar I was using to 
untar. When I used the version of tar that comes with Apple, the first 
set of errors disappeared.

The second one though didn't disappear I didn't have Macports on my 
laptop. So, I picked your suggestion of compiling Frama-C from the 
source. I followed the instructions on wiki and then while I was 
installing Beryllium, I got another error. The make didn't go through 
because of the following error:

Linking      bin/ptests.byte
File "ptests/ptests.ml", line 57, characters 6-15:
Error: This expression has type
          ?temp_dir:string -> string -> string -> string
        but an expression was expected of type string -> string -> string
make: *** [bin/ptests.byte] Error 2

And as expected the following also didn't go through:

sh-3.2# sudo make install
Generating   destination directories
Copying to   shared files
Copying to   binaries
cp: bin/toplevel.opt: No such file or directory
make: *** [install] Error 1

Before writing this email, I decided to try once more installing 
Beryllium binaries. And surprisingly it worked. :) I am not sure this is 
because of installing Macports or it is because of the separate 
installations I did  before trying to compile Beryllium.

Thanks again,
naghmeh

On 20/04/10 3:26 PM, Pascal Cuoq wrote:
> Hello,
>
>    
>> I am a new user of Frama-C. I am trying to install the Frama-C Beryllium (2)
>> for Mac OS X 10.5.8 Intel (the distribution that includes Why 2.23). I have
>> followed all the instructions in the README file. But I get the following
>> error.
>>
>> Macintosh-2:~ nghafari$ frama-c-gui -slevel 10 first.c
>> [kernel] warning: cannot load file
>> "/usr/local/Frama-C_Be/lib/frama-c/plugins/._Jessie.cmxs" (dynlink error
>> "error loading shared library:
>> dlopen(/usr/local/Frama-C_Be/lib/frama-c/plugins/._Jessie.cmxs, 138): no
>> suitable image found.  Did find:
>>      
> These files should not exist. A likely explanation is that you used a tar other
> than "Apple tar", which is installed in /usr/bin/tar. I can only try to explain
> these two warning and hope that the later errors have the same cause,
> and thus will be fixed at the same time.
>
> Here is my take, but this is only my guess of
> what happened and why, so anyone feel free to correct me:
>
> Apple loves to associate metadata with files. It started with "resource forks"
> in the 80s and while the metadata goes by another name nowadays,
> it's still the same principle and still something that filesystems other than
> HFS+ cannot accomodate.
>
> In order to avoid repeating the fiasco of the resource forks in the
> 80s with modern
> USB disks and samba mounts, however, it was decided that the metadata
> of file foo would go in a file named ._foo each time foo would be copied
> to a filesystem that did not support metadata. The tar format, which was
> fixed a long time ago for the excellent reason of bidirectional compatibility,
> was considered like a filesystem like any other filesystem that does not
> understand metadata.
>
> The tar binary provided by Apple knows both how to encode a file metadata
> into a ._ file and to recreate it when such an archive is untarred on
> a filesystem
> that supports it. But if you untar this file with another tar -- say, the
> original GNU tar that a distribution of source packages for Mac OS X
> decided to install for unfathomable reasons -- then ._ files will be created
> and lay there.
>
> In the case of Frama-C there is nothing important in these files, but Frama-C
> looks for all files with the .cmxs extension in
> /usr/local/Frama-C_Be/lib/frama-c/plugins/
> at each launch and tries to load these files as plug-ins. Since a file such
> as /usr/local/Frama-C_Be/lib/frama-c/plugins/._Jessie.cmxs is only a short
> file destined to encode metadata temporarily, it is not a valid plug-in.
>
> The solution would be to erase /usr/local/Frama-C and to make sure that
> you use /usr/bin/tar for untarring it again. In fact, if my guess is correct,
> it would save you other headaches to make sure that Apple's tar is
> always used in preference to the other tar you have.
>
>    
>> Tue Apr 20 12:49:37 Macintosh-2.local frama-c-gui[1243]<Error>:
>> GCGetStrikeMetrics failed: error 4.
>>
>> (frama-c-gui:1243): Pango-CRITICAL **: pango_glyph_string_set_size:
>> assertion `new_len>= 0' failed
>> Bus error
>>      
> I have not explanation for these messages, but if my previous guess that
> you use a distribution of Unix software such as MacPorts or Fink, it might
> be worth trying to rename temporarily any .gtk* configuration file that you
> have in your home directory before launching Frama-C. Frama-C uses
> gtk+. While all the necessary libraries (compiled thanks to MacPorts)
> are packaged in the archive and are installed in /usr/local/Frama-C_Be to
> avoid clashes for MacPorts users, a user's personal configuration files
> can still cause problems when interpreted by Frama-C's version of
> these libraries (for instance if the refer to themes that are not provided
> in Frama-C).
>
> To summarize:
>
> - are you using MacPorts?
> - what does "which tar" say on your computer?
> - perhaps reinstall while making sure of using Apple tar
> - or perhaps you might be better served by compiling Frama-C from
> sources after having used MacPorts to install all of those dependencies
> it has packages for. Jens Gerlach posted a laundry list for doing that a
> while ago:
> http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-September/001390.html
> Note that this message is referenced from the excellent Frama-C wiki:
> http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:start
>
> Pascal
>
> _______________________________________________
> 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
>