Re: Appetite for Frama-C annotations?

Hi there,

I played a lot with frama-c a long time ago.
Frama-c annotations are very verbose and the result is highly dependent on
the skills of the annotator.

Keeping it up-to-date on such a large project with high-speed development
will be, in my very humble opinion, extremely difficult.
Perhaps on a sub-project like libpq ?

--
Laurent "ker2x" Laborde

On Wed, Dec 8, 2021 at 3:45 PM Colin Gilbert <colingilbert86(at)gmail(dot)com>
wrote:

> I've been becoming more and more interested in learning formal methods
> and wanted to find a good project to which I could contribute. Would
> the development team appreciate someone adding ACSL annotations to the
> codebase? Are such pull requests likely to be upstreamed? I ask this
> because it uses comment syntax to express the specifications and some
> people dislike that. However, as we all know, there are solid
> advantages to using formal methods, such as automatic test generation
> and proven absence of runtime errors.
>
> Looking forward to hearing from you!
> Colin
>
>
>