89 lines
2.8 KiB
Plaintext
89 lines
2.8 KiB
Plaintext
$NetBSD: verification,v 1.2 2019/06/17 17:45:18 kamil Exp $
|
|
|
|
NetBSD Verification Roadmap
|
|
===========================
|
|
|
|
This roadmap covers things that we intend or would like to do pursuant
|
|
to verification and quality control.
|
|
|
|
The following elements, projects, and goals are relatively near-term:
|
|
|
|
1. Cut down the Coverity backlog
|
|
3. Deploy clang-static-analyzer
|
|
|
|
The following elements, projects, and goals are longer-term:
|
|
|
|
4. mint
|
|
5. Database-driven program analyzer
|
|
|
|
The following elements, projects, and goals are rather blue-sky so far:
|
|
|
|
6. Use Frama-C to verify fsck_ffs
|
|
|
|
|
|
Explanations
|
|
============
|
|
|
|
1. Cut down the Coverity backlog
|
|
|
|
Coverity provides us with free analysis reports, which we sometimes
|
|
handle and sometimes don't. Apparently though Linux has a lower number
|
|
of Coverity hits per line than we do; that seems fundamentally wrong
|
|
and something that should get attention. Most of the problems Coverity
|
|
finds are pretty easily fixed, or are false positives.
|
|
|
|
- As of January 2017 coypu has been working on this. Christos often
|
|
also fixes these.
|
|
- There is currently no clear timeframe or release target.
|
|
- Contact christos for further information.
|
|
|
|
|
|
3. Deploy clang-static-analyzer
|
|
|
|
There is some makefile support for running clang-static-analyzer, but
|
|
it doesn't get done regularly. This should probably get added to the
|
|
autobuilds.
|
|
|
|
- As of January 2017 nobody is known to be working on this.
|
|
- There is currently no clear timeframe or release target.
|
|
- Contact joerg for further information.
|
|
|
|
|
|
4. mint
|
|
|
|
A while back dholland started on a replacement for the existing lint,
|
|
since lint is not really smart enough to be useful and its code is
|
|
only marginally maintainable. The code is in othersrc, but it needs
|
|
some tidying before anyone else tries hacking on it.
|
|
|
|
- As of January 2017 nobody is known to be working on this.
|
|
- There is currently no clear timeframe or release target.
|
|
- Responsible: dholland
|
|
|
|
|
|
5. Database-driven program analyzer
|
|
|
|
In the long run we would like to have a program analyzer that can
|
|
scale to the whole kernel and can do differential analyses across
|
|
different versions. This is a nontrivial project though.
|
|
|
|
- As of January 2017 nobody is known to be working on this.
|
|
- There is currently no clear timeframe or release target.
|
|
- Contact: dholland
|
|
|
|
|
|
6. Use Frama-C to verify fsck_ffs
|
|
|
|
Frama-C is a framework for doing formal verification of C code using
|
|
(mostly) precondition/postcondition specs. It is not everything one
|
|
necessarily wants in a verification framework; but on the other hand
|
|
it exists and people do use it.
|
|
|
|
fsck_ffs seems like a good candidate for this because it's
|
|
mission-critical and what it needs to do is comparatively well
|
|
understood even in detail. However, the code may be too messy.
|
|
|
|
- As of January 2017 nobody is known to be working on this.
|
|
- There is currently no clear timeframe or release target.
|
|
- Contact: dholland
|