↓Skip to main content

How to Set Up Unit Tests and SPARK Proofs

Table of Contents

Hello again! In today’s post I am going to show you how I organise the project so that I can comfortably switch between normal builds, unit tests, and full SPARK proofs — with or without tasking and with logging turned on or off.

For this I use the adacl_embedded crate as an example. It contains both proof and unit tests, and has three variants of each that are tested and proven separately. This is the most complex case and will show you how the set-up scales nicely.

Chapter 1: Directory Structure #

The generally suggested approach is to place the tests and proofs into separate child crates inside the main crate. This way each configuration lives in its own top-level directory so that GNAT and Alire can keep object files, executables and proof artefacts completely separate. It prevents one build from contaminating another and makes it trivial to switch between them with a single cd and alr build (or spark prove), or to set everything up in one Visual Studio Code workspace.

adacl_embedded
├── .vscode                  # VS Code settings (shared by most configurations)
├── alire                    # Alire workspace files
├── config                   # Project-wide configuration
├── lib                      # Pre-built libraries
├── obj                      # Main object directory
├── share                    # Shared resources
├── src                      # Main source code
│
├── prove_log_off            # SPARK proof – logging disabled
│   ├── alire
│   ├── bin
│   ├── config
│   ├── obj
│   └── src
│
├── prove_no_tasking         # SPARK proof – tasking disabled
│   ├── alire
│   ├── bin
│   ├── config
│   ├── obj
│   └── src
│
├── prove_tasking            # SPARK proof – full tasking enabled
│   ├── alire
│   ├── bin
│   ├── config
│   ├── obj
│   └── src
│
├── test_log_off             # Unit tests – logging disabled
│   ├── .vscode
│   ├── alire
│   ├── bin
│   ├── config
│   ├── obj
│   ├── share
│   └── src
│
├── test_no_tasking          # Unit tests – tasking disabled
│   ├── .vscode
│   ├── alire
│   ├── bin
│   ├── config
│   ├── obj
│   ├── share
│   └── src
│
└── test_tasking             # Unit tests – full tasking enabled
    ├── .vscode
    ├── alire
    ├── bin
    ├── config
    ├── obj
    ├── share
    └── src

Explanation:

  • prove_* directories are used when I run spark prove.
  • test_* directories are used when I run the unit test harness.
  • The suffixes _log_off, _no_tasking and _tasking reflect the compile-time switches I set in the corresponding alire.toml and .gpr files, which makes everything easier for humans to understand.

Note that with current versions of Alire the child crates no longer need to start with test, but I keep the old naming convention anyway for clarity.

Chapter 2: Executing Tests #

Now that we have a sensible directory layout, let’s look at how I actually run the tests and proofs.

Tests are executed with the simple command alr test. However, by default alr test only builds the crate. If you actually want your unit tests (or proofs) to run, you need to add a test action.

Simple AUnit Test Crate #

For AUnit tests you simply call the test binary. I use this setup in all the test_* child crates. Remember to add the dependency on aunit and on your own crate under test.

[build-profiles]
adacl_embedded = "validation"

[[depends-on]]
adacl_embedded = "^7.1.0"
aunit = "^26.0.0"

[[pins]]
adacl_embedded = { path = ".." }

[[actions]]
type = "test"
command = ["alr", "run"]
directory = "."

Simple SPARK Prove Crate #

For a SPARK proof you just call gnatprove. I use this in all the prove_* child crates.

[build-profiles]
adacl_embedded = "validation"

[[depends-on]]
adacl_embedded = "^7.1.0"
gnatprove = "^16.1"

[[actions]]
type = "test"
command = ["alr", "gnatprove"]
directory = "."

Simple Main Crate #

Of course, what you really want is to test the main crate itself — and you can do exactly that by adding a test action to it as well.

A word of warning! alr test is what the continuous integration system of the Alire Index uses to check your crate. Once you add a test action to your main crate, you are committing to keep all your tests in perfect order. From that moment on, “Passed 499 out of 500 tests” is no longer acceptable. But then again — you are programming in Ada, so you already knew that.

[[actions]]
type = "test"
command = ["alr", "--chdir=test", "run"]
directory = "."

Note: At the time of writing there is a small issue with the directory setting, so I use the --chdir=test workaround instead.

Complex Main Crate (Multiple Child Crates) #

The simple approach works fine for a single child crate. When you have several (as in adacl_embedded), I wrote two small scripts that run all the tests and proofs in succession.

The action definition then looks a little more involved because you need different scripts for Unix-like systems and Windows:

[[actions]]
[actions.'case(os)'.linux]
type = "test"
command = ["/bin/bash", "ci-verify.sh"]
directory = "."

[actions.'case(os)'.macos]
type = "test"
command = ["/bin/bash", "ci-verify.sh"]
directory = "."

[actions.'case(os)'.windows]
type = "test"
command = ["powershell", "-ExecutionPolicy", "Bypass", "-File", "ci-verify.ps1"]
directory = "."

In its simplest form the script just calls one test after another. My own scripts are rather over-engineered with colours and clear status messages — you can see the full versions by fetching the crate with:

alr get adacl_embedded

Note: The explicit /bin/bash path is needed because the execute permission is lost in transit when Alire unpacks the crate.

Chapter 3: Setting Up Visual Studio Code #

When I started developing for the Raspberry Pi Pico I also switched to Visual Studio Code, as it was the only IDE in which I could reliably get GDB working. Fortunately, VS Code is very flexible and copes well with slightly unusual project layouts like ours.

Workspace #

I added all the crates to the workspace folders section. This lets me access the main crate and every test/proof variant from a single workspace, so I no longer need to keep switching between different workspaces.

Here is the core of my .code-workspace file:

{
  "folders": [
    { "path": "." },
    { "path": "prove_log_off" },
    { "path": "prove_no_tasking" },
    { "path": "prove_tasking" },
    { "path": "test_log_off" },
    { "path": "test_no_tasking" },
    { "path": "test_tasking" }
  ],
  "settings": {
    "ada.alireDiagnostics": true,
    "ada.defaultCharset": "utf8",
    "ada.foldComments": true,
    "ada.renameInComments": true,
    "ada.projectFile": "adacl_embedded.gpr",
    "ada.scenarioVariables": {
      "adael.Variant": "tasking"
    },
    "files.associations": {
      "*.ada": "ada",
      "*.adb": "ada",
      "*.ads": "ada"
    }
    ...
  }
}

Tasks #

I also created a task for each individual proof and test run, plus an “all tests” task for convenience. This way I can validate any configuration with a single keystroke.

{
  "version": "2.0.0",
  "tasks": [
    {
      "label": "Ada Build Development",
      "type": "ada",
      "command": "alr",
      "args": ["build", "--development"],
      "group": { "kind": "build" }
    },
    {
      "label": "Ada Validate All",
      "type": "ada",
      "command": "alr",
      "args": ["test"],
      "group": { "kind": "test", "isDefault": true }
    },
    {
      "label": "Ada Validate „Prove Log Off“",
      "type": "ada",
      "command": "alr",
      "args": ["--chdir=prove_log_off", "run"],
      "group": { "kind": "test" }
    },
    {
      "label": "Ada Validate „Prove No Tasking“",
      "type": "ada",
      "command": "alr",
      "args": ["--chdir=prove_no_tasking", "run"],
      "group": { "kind": "test" }
    },
    {
      "label": "Ada Validate „Prove Tasking“",
      "type": "ada",
      "command": "alr",
      "args": ["--chdir=prove_tasking", "run"],
      "group": { "kind": "test" }
    },
    {
      "label": "Ada Validate „Test Log Off“",
      "type": "ada",
      "command": "alr",
      "args": ["--chdir=test_log_off", "run"],
      "group": { "kind": "test" }
    },
    {
      "label": "Ada Validate „Test No Tasking“",
      "type": "ada",
      "command": "alr",
      "args": ["--chdir=test_no_tasking", "run"],
      "group": { "kind": "test" }
    },
    {
      "label": "Ada Validate „Test Tasking“",
      "type": "ada",
      "command": "alr",
      "args": ["--chdir=test_tasking", "run"],
      "group": { "kind": "test" }
    }
    ...
  ]
}

Projects for the Child Crates #

You can also create individual project files and workspaces for the child crates. Visual Studio Code will automatically discover them and merge everything into the main workspace. You then have to decide whether you prefer the tasks to live in the main workspace or in the relevant child workspace — both approaches have advantages and disadvantages.