--- layout: fc_discuss_archives title: Message 24 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,

2012/7/10 Jens Gerlach <jens.gerlach at first.fraunhofer.de>:
> 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.
>

That's right, Why is only needed by WP at run-time (and if you intend
to use something other than alt-ergo or Coq).
Regarding your installation notes, as far as I know, one of the
install of WP-0.5 is, as you guessed, unnecessary, as well as the
second install of Frama-C. In other words,
- Frama-C needs to be installed before Why2 and WP-0.5
- Why3 and alt-ergo can be installed completely separately

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile