--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Assignments proof



Hello,

2013/9/3 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>:
> We are using the Jessie and how it does not come installed on new version we
> do not update our version.
>
> Furthermore, we have not experience to compile the source distribution.
>
> But we will look some messages posted in the list and we will try to install
> the new version.

Opam has packages for the latest versions of both Frama-C
(Fluorine-20130601) and Why (2.33), which are compatible (i.e. Jessie
plugin 2.33
can be compiled against Frama-C Fluorine-20130601). I've just checked
that with these versions, the combination of Alt-ergo and Gappa
succeeds in discharging all POs from Jessie (Alt-ergo is used for the
assigns clause, Gappa handles all the floating-point related POs).

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