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] Frama-C compilation: questions on APRON, test error and missing plugin?

Hello,

Pascal Cuoq <Pascal.Cuoq at cea.fr> writes:

> On Feb 27, 2009, at 2:54 PM, David MENTRE wrote:
>> I have successfully compiled Frama-C Lithium on Debian Lenny 5.0 (I
>> can give my installation notes if needed).
>
> We would be happy to have them in order to be able to provide them to
> others, or even to fix what is fixable.

I'll provide them on Monday. As far as I remember, there was no
particular issue on the Frama-C side.

> Note that at this time APRON is used only by the Jessie plug-in
> for trying to find invariants automatically on functions that make
> use of common C string manipulation idioms.

Ok. A few word saying that in the INSTALL might be useful.

[ tests error ]
> A file, minix3_include/string.h, seems
> to be missing. This may be an omission on our part. Again, do not
> worry about it, it does not imply that Frama-C is incorrect or
> mis-installed on your computer.

Ok, good to know.


[ other provers ]
> The page at http://why.lri.fr/ lists haRVey.

Yes, I've seen it just after sending this email. :-) 

Apparently, there are two variants of haRVey (FOL and SAT). Within
Frama-C context, is there any advantage of one over the other?

> I have heard that sources for Simplify were still floating around,
> again please follow the links from the Why webpage and see if
> what you find is acceptable to you (shortcut: you'll probably end up at
> http://secure.ucd.ie/products/opensource/ESCJava2/license.html
> at some point).

Yes, I already had a look at this ESCJava2/license.html page in the
past. The license is clearly not suitable for use as Free Software.

Anyway, Simplify is apparently dead: "We do not plan on doing any
development on Simplify, as the world of first-order theorem provers has
changed quite a bit over the past decade or so. Instead, we are working
on integrating ESC/Java3 with new-generation SMT-LIB provers."
 From: http://secure.ucd.ie/products/opensource/Simplify/

> Although Zenon is not listed on the Why webpage, I think that there
> is a good chance that it is supported:
> http://focal.inria.fr/zenon/

Ok, I'll give it a try. Thank you for the pointer.


Many thanks for the detailed answers,
Yours,
david
-- 
GPG/PGP key: A3AD7A2A David MENTRE <dmentre at linux-france.org>
 5996 CC46 4612 9CA4 3562  D7AC 6C67 9E96 A3AD 7A2A