--- layout: fc_discuss_archives title: Message 70 from Frama-C-discuss on May 2010 ---
[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