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