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



On Tue, 2010-05-18 at 16:14 +0200, Julien Signoles wrote:
> For each (major) release, we aim to provide:
> 1) a source distribution of Frama-C
> 2) a source distribution of Frama-C + Why + Jessie

Ok, once (2) is available I'll give it a try.

> We do not provide a package including Alt-Ergo, but this tool has very 
> few requirements (they are a small subset of the requirements of 

But why not include Alt-Ergo in (2)? Even if it has very few
requirements you have to
- discover that why needs at least one prover
- decide which prover to install
- find the download link
- retrieve, untar, configure and compile it

Especially for new users this may take some time. All of this can be
automated if Alt-Ergo is included in (2). After all, computers should
make life easier.

-Boris