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 <colingilber...@gmail.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 > > >
