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

[Frama-c-discuss] Incremental verification



On Wed, Oct 6, 2010 at 6:57 AM, Boris Hollas
<hollas at informatik.htw-dresden.de> wrote:

>> All in all, you need at least a rudimentary parser for C+ACSL, but nothing too
>> sophisticated: being able to detect changes and to build the call tree
>> are enough.
>
> But Frama-C already has a parser for C+ACSL.

I meant, it does not have to be done in Frama-C, and it doesn't have
to be in OCaml. It can be implemented mostly externally by whoever is
interested, and that person does not have to be fluent in OCaml, a
complaint we often hear about extending Frama-C.

> Maybe it's easier to
> augment the existing parser with a feature to detect and forward changes
> to the subsequent tools in the chain.

It would be possible to compare ASTs. As Virgile said, although not
impossible it's not the easiest way and the easiest way is compare
text (as long as you have been able to locate contracts + functions in
the preprocessed source with precision).

>  In that case, a basis to implement
> incremental verification would also be given for the abstract
> interpretation plugin and any other verification plugin.

The value analysis is not compositional. Even when it checks ACSL
pre-conditions and post-conditions, it only checks that the
pre-condition is ensured by all callers, and that the function
subsequently satisfies the post-condition. It does not check that the
post-condition inherently derives from the pre-condition. In other
words, as soon as one function f is changed, the value analysis has to
analyze again any line of code that can be executed after a call to f,
be it in the caller, in another function called by the caller, or in f
itself if f is called several times.

Context-free analysis in generic initial states as activated by option
-lib-entry could benefit from this feature, though.

Pascal