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] Incremental verification

  • Subject: [Frama-c-discuss] Incremental verification
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Wed, 6 Oct 2010 16:58:00 +0200
  • In-reply-to: <1286373428.7104.228.camel@iti27>
  • References: <1286194386.7104.190.camel@iti27> <AANLkTi=RA4GN7=WWaq019ttoc7dHF6vnHg8QQsUG80+D@mail.gmail.com> <1286373428.7104.228.camel@iti27>
Hello,

Le mer. 06 oct. 2010 15:57:08 CEST,
Boris Hollas <hollas at informatik.htw-dresden.de> a ?crit :

> 
> But Frama-C already has a parser for C+ACSL. Maybe it's easier to
> augment the existing parser with a feature to detect and forward changes

The parser itself has absolutely no way to know what has changed unless
you give it the two versions of the code. And even in this case, the
diff won't be that easy. In my opinion, the best way to handle that is
within your favorite IDE (Eclipse, Emacs, Vim, ...), since it knows
exactly which changes have been made. Chances are that it has already
some notions of C, and as Pascal said, a rudimentary ACSL parser
should be sufficient at this level.

That said, Frama-C can help. In particular, Frama-C Carbon will
probably provide information about the status and dependencies of
each annotation (has it been verified, by which plug-in and under which
hypotheses, including other annotations). That way, an external tool
would be able to decide what impact a change has in term of
verification.

> 
> I don't know anything about the internals of the provers used by Jessie,
> so I don't know if any of them have specific support for caching. But
> caching could also be implemented in Jessie if just the proved VCs are
> cached. If, for example, you just change something in your precondition,
> this should give a considerable speedup. 

Not that much. At Jessie's level, if your precondition changes, most
proof obligations of the given function would have to be done again, as
they more or less all depend of the hypotheses made on the initial
state. Some provers are able to output a proof trace, and we have
on-going projects to take advantage of this trace to refine
dependencies between annotations, but at this point I won't even mention
a version name as a target for release.

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