Adacovex: code/proof/DO-178C HAL/docstring status tool

Releases
,
1

image

Basically wanted proper project badges generated from a CLI like in Golang/Rust for my Ada projects. Hope this would be a useful addition for checking on code quality. Supports parsing SPARK level, unit tests, DO-178 HAL level and docstrings coverage.

Repo URL: GitHub - bladeacer/adacovex: Ada/SPARK code/proof coverage, SPARK level, DO-178C HAL status tool · GitHub

Binary name is adacovex, crate name is covex to comply with policy.

Disclaimer: AI assistance was used for the code.

Awaiting PR merge to Alire, would publish the newer upstream code changes at a later time.

10 Likes
[ANN] adacovex 1.14.0: Multiple Compliance Standards, plenty of QOL updates
2

I am currently on a project that has to do DO-178 certification, but sadly it’s all in C. While this tool would not benefit my current project, I can appreciate what it provides.

Thanks for your contribution to the community!

2 Likes
3

Thanks for your kind words ^_^.

I plan to perhaps add language agnostic support in the long run (Ada has a great way to exposing FFIs to C) as well as some way to check deltas on code coverage on pull requests.

The 1.0.0 PR to Alire has been merged, now I will wait till it shows up on the site and continue with dev.

3 Likes
4

Is it DO-178 HAL or DO-178 DAL? Your screenshot and link don’t match on this.

5

DAL, my bad. :sweat_smile:

Must have made a typo somewhere, thanks for catching it.

1 Like
6

Released 1.1.0 with some fixes made, awaiting PR merge to Alire.

Changelogs:

7

Got adacovex to run on GitHub CI though it is about time gnatprove is listed as an explicit dependency. Needs more polish but once the update is out one can check code coverage changes between each PR or on push. I plan to publish a companion GitHub Action as well as push 1.3.0 to Alire if things go well.

1 Like
8

1.3.0 is out. I plan to polish github actions UX, add a SBOM flag and “bundle” gnatprove itself so it can be easily invoked alongside the binary (using alr).

2 Likes
9

1.5.0 is out. Realised I never published the draft release for 1.3.0.

Changelogs

2 Likes
10

Removed some of the PRs to alire-index since I realised I should not bundle gnatprove as a dep in alire.toml.

11

1.6.0 is out, forgot to mention that we now have a working GitHub Action to run adacovex in CI or on PRs. There are also some other internal refinements.

As usual, PR to Alire will take a while.

Changelogs

Build Provenance Attestation:

P.S. I have some plans for 2.0 though there needs to be fair bit more polish on the UX side of things.

1 Like
12

Forgot to summarise the set of changes, mainly:

  • It does not false positive on third party/deps being SPARK proven
  • The badges now have better text to background contrast (e.g. no more bright background + bright text)
  • Codebase is fully proved now
  • Updated installation docs
  • Shown how to tie SBOM timestamp to git commit so to version control it is deterministic
  • Some other changes to the GitHub Actions set up

P.S. If the project goes well and language agnostic support is done properly for 2.0 I would be interested in submitting a proposal to present about the project at FOSDEM or similar events that are programming/Ada related.

The code is “decent” but not crate of the year quality yet. I will continue working on it.

3 Likes
13

So I have started dogfooding in some sense, my Ada_CRDT project now makes use of adacovex itself. This is probably a good way to find out and address any possible gaps in DX/UX going forward.

I am considering making a Matrix Room once there is demand for it (enough users). If there are any bugs or quirks, do open an issue or better yet a PR at the GitHub.

14

Findings thus far suggest there is a parser bug which skipped certain unproved code.

That being said I am almost there in terms of having a decent caching mechanism as well as consistency between local and CI runs of adacovex. Hopefully I can drop another release soon.

P.S. Contemplating creating a Matrix room.

Edit: Working on a fix now, also noting the differences in output format between gnatprove v15 and 16.

1 Like
15

Update: The parser is now more honest about unproved code.

Will be working on slowly getting back (actual) SPARK Platinum and write proper proofs.

1 Like
16

1.9.0 is out :smiley:

tldr;

  • parser is now honest
  • you can version pin gnatprove, tested on gnatprove v15/16
  • CI threshold gates (so you can require x level of SPARK and y level of docstrings, tests and proofs)
  • dev deps also included in SBOM as dev deps
  • cached results

Changelogs

Build Provenance Attestation:

Do look at 1.8.0 and 1.7.0 changelogs as well, there are some other changes they included but mostly relating to code quality.

2 Likes
17

Will make a new post soon, some exciting changes are coming in the newer versions of adacovex.

2 Likes
18

1.14.0 dropped, made a new post on it here: [ANN] adacovex 1.14.0: Multiple Compliance Standards, plenty of QOL updates