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] 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
>