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

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