--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Incremental verification



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