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