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] RE : [support-caveat] Questions about the Lithium beta 1 release

  • Subject: [Frama-c-discuss] RE : [support-caveat] Questions about the Lithium beta 1 release
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Thu, 4 Dec 2008 10:21:52 +0100
  • References: <1228218803.32587.7.camel@ossiriand>
Some answers that has not made it yet to the frama-c-discuss list,
for the record...

>   1.1. We are very happy with this feature, but it works only in
> bytecode mode (Lithium beta 1). Will it eventually work with native code
> also?

Yes! It already does if you are willing to install the release candidate
for OCaml 3.11.0. See
http://groups.google.com/group/fa.caml/browse_thread/thread/0ec06867774922fd?pli=1

The feature that you need in order to get dynamic plugins
*and* native code is called "dynlink". It is supported for pretty much
all target OCaml architectures. Look for recent messages concerning
dynlink in the OCaml forums for details, and see recent
messages bu Julien in this list for more details about dynamic plug-ins
in Frama-C.

> 2. On machine dependent parameters.

> One of the tool general options reads:
>  -machdep machine : use [machine] as the current machine dependent
>configuration.
> Can you tell me more on how to fill in this configuration file?

This option expects the name of a target platform. A list of
supported platforms can be
obtained through "-machdep help".
 
>Section 2.4.2 of http://frama-c.cea.fr/download/frama-c-manual-Lithium-
>en.pdf claims "an autodetection program is provided in order to check
>the hypotheses mentioned in section 2.4.1, as well as to detect the
>endianness of the target and size of each C type".
>I failed to find such a program. Could you tell me more on this?

The documentation is wrong. It should say "please contact the 
Frama-C developers if you want to obtain an auto-detection program
for an architecture that is not currently supported."
We would prefer to hear about new architectures that people
want to target.

>  3.2. We have been able to run Frama-C on Linux RHEL 4 untill
>Helium-20080701+dev2, but on the GUI no longer works with
>Lithium-20081001+alpha1 and with Lithium-20081002+beta1. This is a
>nuisance, because it is hard to experiment on impact analysis that way.

As someone who has been trying for a year to build a usable binary package
for Frama-C for an OS with the same limitations as RHEL 4 for different
reasons (the required libraries, in adequately recent versions, are not
part of the OS), I am in a good position to tell you that it is a lot of tedious,
unrewarding work. It will happen. We are working on it.

Pascal