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] Problem with predicate and location labels

  • Subject: [Frama-c-discuss] Problem with predicate and location labels
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Thu, 17 Feb 2011 17:41:51 +0100
  • In-reply-to: <1297959573.1185.33.camel@iti27>
  • References: <a3ffffe11e168693bb7066d5932fe18a.squirrel@webmail.informatik.htw-dresden.de> <20110216184311.7d78da4e@is010235> <1297933420.1735.76.camel@iti27> <20110217164835.757bc8f0@is010235> <1297959573.1185.33.camel@iti27>
Le jeu. 17 f?vr. 2011 17:19:33 CET,
Boris Hollas <hollas at informatik.htw-dresden.de> a ?crit :

> 
> Yes, you're right, some manual intervention is necessary. Is this what
> you mean with "to transform the spec  into a statement
> contract at the call point"?

Well, this is not a manual intervention. The transformation I'm
referring to is simply the substitution of formals by actual parameters
and of \result by the lval were the returned value is stored. If you
stick to a contract statement at the call point, this is all you need
to do.

> However, my code doesn't have loops, so most steps are quite easy.
> 

Well, as soon as you have pointers, assignments themselves become an
issue, as you have to take potential aliases into account. Things
become messy very quickly.

> I've done some experiments with the WP and RTE plugins, but so far I
> can't verify code that verifies with Jessie.
> 
> What are the differences between what the RTE plugin does for WP and
> what the apron library does for Jessie?

Both are completely orthogonal. Apron library is (was? I'm not sure of
the current status of this part of Why) used to generate invariants
(especially the "trivial" ones such as 0<=i<=n for the index, that are
very boring to write but essential to complete proofs). RTE generates
what appears in Jessie/Why as Safety proof obligations. But while this
is handled internally by the jessie program (and thus completely
opaque from a frama-c point of view), RTE just generates plain ACSL
annotations, which means that WP is not the only plugin that can be
used to verify these POs: they are registered in Frama-C's kernel like
all annotations, and the user is free to use whatever combination of
plugins s/he wants to ensure that they hold.

-- 
E tutto per oggi, a la prossima volta.
Virgile