--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on December 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP: Sodium version cannot prove a property that Neon version can prove



Hello,

On 12/09/15 17:54, Loïc Correnson wrote:
> Hi,
> My only possible answer is that everything is proved with (on-going, not yet released) Magnesium version and alt-ergo 0.99.1
> May I suggest you to upgrade to, let say, opam versions ?

Sodium-20150201 is the latest Frama-C version available via opam. I
upgraded Alt-Ergo to version 0.99.1, but the results are the same:
everything is proved with Neon but not with Sodium.

> Sorry, I don’t have time right now to investigate on older versions.

Okay, I am fine with your answer that it works again with the upcoming
Magnesium version and will not worry about the Sodium result. Thanks for
testing it.

Regards,
Timo