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: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Wed, 6 Oct 2010 09:18:10 -0700
  • 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>
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