Re: frama-c_20161101+silicon+dfsg-1_amd64.changes ACCEPTED into unstable
Hi Mehdi,
On Thu, Dec 22, 2016 at 12:06:15AM +0100, Mehdi Dogguy wrote:
> Hi Ralf,
>
> On 21/12/2016 21:03, Ralf Treinen wrote:
> > how do you know that why will not be part of stretch ?
> >
>
> Why has been removed from testing since 2016-02-14 and why3 is now part
> of Stretch. I have assumed the former has been dropped in favor of the
> latter. Apologies if this is not the case. I'd be happy to restore the
> Recommends statements if that's useful for someone.
this is not the case. Since the 2.36 upstream release of why, why
only contains the krakatoa and jessie plugins for frama-c. These now
generate code in the why3 language, which has to be proven using why3.
Only the "why" binary itself has gone. That is, why now depends both
on frama-c and why3.
The reasons for the removal of why from testing where different ones,
and should be fixed now. why 2.36-3 should migrate back into testing
in the next days.
Cheers -Ralf.
Reply to: