--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on July 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Compiling Frama-C and why



Hello Boris,

attached are some installation notes of mine for WP (in German-).
If you find a a simpler way then please tell me.
(They are for nitrogen, but currently I am using the nitrogen package that comes with ubuntu 2012-04.)

Regarding the circular dependency, I understood the issue as follows:
WP can use alt-ergo directly (without why). To use other provers you have to install why first.
For details see our installation notes.

Regards

Jens


On 10 Jul 2012, at 16:31, Boris Hollas wrote:

Hello,

I've upgraded my system and I'm reinstalling Frama-C. Configuring Frama-C gives

configure: WARNING: why not found
configure: WARNING: wp partially enabled because why missing.
configure: WARNING: why-dp not found
configure: WARNING: wp partially enabled because why-dp missing.

On the other hand, the configure script for why2 warns that Frama-C can't be found, hence Jessie can't be installed. So it seems there's a circular dependency between why and Frama-C. In what order should I compile the sources?

Begards,
Boris

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr>
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: installation.txt
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120710/7fca1a6e/attachment.txt>