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
- Subject: [Frama-c-discuss] Small function on buffer doesn't verify
- From: Julien.Signoles at cea.fr (Julien Signoles)
- Date: Tue, 18 May 2010 14:23:18 +0200
- In-reply-to: <1274181525.2155.29.camel@iti27>
- References: <1273591300.4338.8.camel@iti27> <4BEF960F.6070300@inria.fr> <1274100093.2155.8.camel@iti27> <4BF13DCE.40802@cea.fr> <1274167523.2155.15.camel@iti27> <4BF2425B.5010503@cea.fr> <4BF26A5D.9050103@inria.fr> <4BF26E48.50205@cea.fr> <1274181525.2155.29.camel@iti27>
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
- Follow-Ups:
- [Frama-c-discuss] Small function on buffer doesn't verify
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] Small function on buffer doesn't verify
- References:
- [Frama-c-discuss] Small function on buffer doesn't verify
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] Small function on buffer doesn't verify
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] Small function on buffer doesn't verify
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] Small function on buffer doesn't verify
- From: Julien.Signoles at cea.fr (Julien Signoles)
- [Frama-c-discuss] Small function on buffer doesn't verify
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] Small function on buffer doesn't verify
- From: Julien.Signoles at cea.fr (Julien Signoles)
- [Frama-c-discuss] Small function on buffer doesn't verify
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] Small function on buffer doesn't verify
- From: Julien.Signoles at cea.fr (Julien Signoles)
- [Frama-c-discuss] Small function on buffer doesn't verify
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] Small function on buffer doesn't verify
- Prev by Date: [Frama-c-discuss] Small function on buffer doesn't verify
- Next by Date: [Frama-c-discuss] Small function on buffer doesn't verify
- Previous by thread: [Frama-c-discuss] Small function on buffer doesn't verify
- Next by thread: [Frama-c-discuss] Small function on buffer doesn't verify
- Index(es):