--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on October 2010 ---
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