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

[Frama-c-discuss] proving a contract



Sorry for the various typos in my previous mail... I have one additional remark.

On Tue, Mar 27, 2012 at 10:49 AM, Boris Yakobowski <boris at yakobowski.org> wrote:
> Since your are referring to Skein, I am assuming you are using ?the
> Value analysis (we usually use the terminology "prover" for
> weakest-preconditions-based plugins such as Jessie or WP). From what I
> can check, your spec for Skein_256_Init is fine.

I was actually referring to your ensures. As you are probably aware,
your assigns clauses are incomplete for the moment. Notice that the
Value analysis does not use them at all when the body of a function is
present, and does not check them either. So unless you want to use
Jessie or the WP module, you won't be able to verify them formally.
Should you decide to use those plugins, keep in mind that they do not
currently understand the \initialized predicate, which is the main
source of problem in the analysis of the Skein code.

HTH,

-- 
Boris