Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] proving a contract

  • Subject: [Frama-c-discuss] proving a contract
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Tue, 27 Mar 2012 11:06:13 +0200
  • In-reply-to: <CABbVA-Csjgd3w7iXLnQr=AFeepg7ynEAJr=Thoz7b961UJz9ug@mail.gmail.com>
  • References: <4F716A54.8000307@magwas.rulez.org> <CABbVA-Csjgd3w7iXLnQr=AFeepg7ynEAJr=Thoz7b961UJz9ug@mail.gmail.com>
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