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] Frama-C Boron and Why 2.24 package for Mac OS X

  • Subject: [Frama-c-discuss] Frama-C Boron and Why 2.24 package for Mac OS X
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Sat, 24 Apr 2010 09:05:17 +0200
Hello,

You can download from the URL below a package with
Frama-C 20100401 and a patched Why 2.24
for the Intel Mac (Leopard and Snow Leopard):

http://www.mediafire.com/file/qm0tdtkmzyt/frama-c-Boron-20100401_why-2.24p_OSX_intel.tryit.tar.bz2

Note the absence of "I am proud to announce" idiom
in this message. This is not an official release.
The dependencies of Frama-C have changed since the
last version and the whilelist of files to include in the
release, which took several iterations to get right
in the past, must be adjusted in consequence.

This is not a scary "test" or "beta" release either.
This is a "tryit" release. If you have an Intel Mac,
just try it.

Pascal
__

This is the binary release of Frama-C for Mac OS X. It contains
software which is provided as binaries as a convenience only. Each piece
of software is covered by its respective license. The SVN repository
of MacPorts of April 23, 2010 should be considered as the reference for
the distributed software. The MacPorts SVN repository contains links to
source code, for those pieces of software which make this a condition
to re-distribution.

In addition to software from MacPorts, this package contains
OCaml 3.11.2 and alt-ergo 0.9.

Please untar the archive as root in /
It will *not* work from another location.
You should probably install the included DejaVu fonts
(see the first bug in the following list).
You should also put the directory /usr/local/Frama-C_B/bin
in your path.
Once all this is done, you are set up.

To play the tutorial from http://frama-c.com/try_out.html, type:

frama-c-gui -slevel 10 first.c

This distribution includes the Jessie deductive verification plug-in.
If you wish to compile external plug-ins, you must use the
provided OCaml compiler in /usr/local/Frama-C_B/ocaml-3.11.2


Some known bugs with this binary distribution:

* The display of unicode characters is broken with the default settings.

A workaround is to install the "DejaVu Sans" and "DejaVu Sans Mono" fonts
provided in the folder /usr/local/Frama-C_B/dejavu_fonts.

To install the fonts, open the files "DejaVuSans.ttf" and "DejaVuSansMono.ttf"
and click the button "Install font" that appears in the Font Book dialog.

Note: this workaround shouldn't be necessary. When it is used by the
system (as opposed to pango), the Monaco font (for instance) falls back to
another more complete font for the unicode characters that are missing.
If someone knows how to fix this, please contact me.

* The package should include a Mac OS X-ish theme, to make appearance,
keybindings, ... closer to a native Mac OS X application.

* On first launch, Why requires the user to run the why-config program:
This issue is not specific to this distribution. Why needs to detect which
automatic provers are installed. Only the automatic prover alt-ergo
is provided in this distribution, but you can install any other prover.
If you install more Why-supported provers, make sure they are in your PATH
and run why-config again.

* On first use, displaying the call graph takes a long time:
Again, this is not specific to this distribution. The first time a graph
is displayed, some fonts need to be generated in ~/.fontconfig.
These are cached for subsequent use.