--- layout: fc_discuss_archives title: Message 69 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 Julien,

> the Simplify license prevents us to redistribute this tool within 
> Frama-C: "You may download, modify and redistribute the software to 
> individuals for personal, non-commercial purposes free of charge [...]"

ok, that's a problem. I'll ask the Simplify people if they can change
the license to a more liberal one.

> > - 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. 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. 

So, if we want to foster the use of formal verification, we must at
least ensure that the installation is easy. 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, 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.

BTW, are there binary packages for Boron?

Regards,
Boris