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] Small function on buffer doesn't verify

Hello Boris,

Boris Hollas a ?crit :
I'll ask the Simplify people if they can change
> the license to a more liberal one.

Quite optimistic: good luck ;-).

>>> - installation instruction that lists additional required packages
>>> for download on the frama-c site?
>> Are the "compilation instructions" [1] not enough?
>> [1] http://frama-c.com/install-boron-20100401.html
> 
> I haven't tried to install Boron yet so I can't judge on this, but I
> found the installations instructions for Beryllium 2 not sufficient. 

They have been improved for Boron.

I
> had lots of trouble compiling it, see
> http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-April/001885.html. Also, our sysadmin as well as two CS students of mine weren't able to install Frama-C + Jessie + GUI on Suse Linux. 

I don't know if someone already successfully compiled Frama-C on Suse Linux.

> So, if we want to foster the use of formal verification, we must at
> least ensure that the installation is easy. 

You're fully right. Nevertheless I know several universities/engineering 
schools where sysadmins successfully install Frama-C for teaching formal 
methods.

A lot of users seem to use
> Frama-C with the Jessie plugin. For these users, a tarball that contains
> Frama-C, Jessie, why, alt-ergo plus any other software that is not
> readily available through the package management system

Which package management system? There is a variety of such systems in 
the Linux world... By the way, there are now Debian and Ubuntu packages 
thanks to the excellent job of Mehdi Dogguy.

, together with
> instructions on which additional packages to install would save a lot of
> work. In that case, it might be as easy as running
> apt-get install p1 p2 p3 ... pk 
> ./configure && make install 
> to start verifying C-code, at least on Ubuntu and Debian.

The installation instructions of Frama-C Boron list the required 
packages for compiling Frama-C on Ubuntu Lucid Lynx 10.04.

> BTW, are there binary packages for Boron?

For each (major) release, we aim to provide:
1) a source distribution of Frama-C
2) a source distribution of Frama-C + Why + Jessie
3) binary distributions for Windows OS and Mac OS X including Frama-C + 
Why + Jessie + all the requirements

At this day, only (1) is provided for Boron but (2) and (3) should be 
released in a close future.

We do not provide a package including Alt-Ergo, but this tool has very 
few requirements (they are a small subset of the requirements of 
Frama-C): it should be very easy to install.

We do not provide binary packages for Linux: that is mainly the job of 
Linux Packagers.

--
Julien