--- layout: fc_discuss_archives title: Message 67 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 12:39 +0200, Julien Signoles wrote:
> Claude Marche a ?crit :
> > And for me, with Boron+Why 2.26, it is 100% proved by any prover below
> > 
> > Alt-Ergo 0.91
> 
> It is not 100% proven by Alt-Ergo 0.9: Alt-Ergo 0.91 is better than 
> Alt-Ergo 0.9 on this example :o). However it seems that Alt-Ergo 0.91 is 
> not yet available on http://ergo.lri.fr.

With Simplify, I was able to prove the postcondition.

I will file a bug report/change request for the issue with #define and
const.

For Boron, is it possible to provide a tarball that includes
- Frama-C
- Jessie
- why
- Simplify
- a makefile
- installation instruction that lists additional required packages
for download on the frama-c site?