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