--- layout: fc_discuss_archives title: Message 68 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



Boris Hollas a ?crit :
> I will file a bug report/change request for the issue with #define and
> const.

OK.

> For Boron, is it possible to provide a tarball that includes
> - Frama-C
> - Jessie
> - why

Yes it could be done since Why-2.26 is now released.

> - Simplify

At least one other Frama-C user complains off-list that Simplify is not 
a free software. I am not a lawyer but I guess the following sentence of 
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 [...]"

Anyway why including just a prover only useful for an external plug-in 
(even it is a major one)? If we follow this way, one day we will provide 
all existing (even non-free) provers and the transitive closure of all 
the requirements (including a linux kernel at the end?)... We have 
chosen a tractable limit by including only ocamlgraph within Frama-C 
since we usually require (at least) the last version of this library. 
All other requirements are not provided in the source distribution.

> - a makefile

We already provide a Makefile for Frama-C and another for Why. So you 
just have to do something like "./configure && make && sudo make install 
&& cd why && ./configure && make && sudo make install".

Thus I think that there is no really need to provide one additional 
not-so-easy-to-maintain Makefile. Ok Frama-C is an open source project: 
fill free to contribute ;-).

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

--
Julien