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 Frama-c-gui

On Thu, Mar 3, 2011 at 6:03 PM, Jens Gerlach
<jens.gerlach at first.fraunhofer.de> wrote:
> Why don't you use the Boron release?
> There are also Ubuntu package for this Release.

Well, I think the case is more that there are Beryllium packages for
some Ubuntu versions (old), and Boron packages for other Ubuntu
versions (recent). So it's more the question of whether Sali wishes to
upgrade to a more recent Ubuntu or not (not that I recommend such a
drastic measure at this time).

I would recommend to compile Carbon. Using the Ubuntu package system,
it is not too hard. However, I cannot guarantee that whatever
particularity of your system that prevents Beryllium from working will
not prevent Carbon from working. Beryllium may have been inferior to
Boron, but the value analysis and the GUI were already at that time
working better than what you describe. You might compile only Frama-C
from source, or Frama-C plus the lablgtk library, or these two plus
OCaml.

Alternately, stick to the command-line version frama-c. It is more
versatile and every documented value analysis verification task can be
done with only the commandline, and is actually more comfortable to do
this way when you are used to it. Do not worry about Jens's warning.
The value analysis was working pretty well in Beryllium, and his own
experience is with another part of Frama-C.

Lastly, are you actually using the "frama-c -val" and "frama-c-gui
-val" commandlines, with nothing else? There was a bug long ago when
no file was specified on the commandline. But that was ages ago. It
must have been fixed in Beryllium. Just in case, try "frama-c-gui -val
somefilethatexists.c" before starting anything complicated.

Pascal