--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on February 2009 ---
[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