# CBMC Batch

Running CBMC Batch jobs for a project.

## Expected Directory Structure

    project
    │   ...   
    │
    └───.cbmc-batch
    │   │   ...
    │   │
    │   └───jobs
    │       └───job1
    │       │   |    Makefile
    │       │   |    cbmc-batch.yaml
    │       └───job2
    │       │   |    Makefile
    │       │   |    cbmc-batch.yaml
    │       ...

It is expected that the repository contains a directory `.cbmc-batch`, which itself contains a directory `jobs`. Each directory in `.cbmc-batch/jobs` should correspond to a CBMC Batch job. Each job directory must contain a `Makefile` to be used by CBMC Batch to build the goto for CBMC and a `cbmc-batch.yaml` file to provide CBMC Batch options and provide an expected substring in the result of the CBMC run.

## Running Locally

In order to start the CBMC Batch jobs and check results locally, you need to have installed CBMC Batch.

You can start the CBMC Batch jobs locally by running

    bash cbmc-batch.sh -s

You can then check CBMC Batch results locally by running

	bash cbmc-batch.sh -e

This will run until all the jobs have finished and output results in `results.txt`.

You can clean up the local CBMC Batch bookkeeping files by running

    bash cbmc-batch.sh -c

The options can be combined, e.g. the following will start the jobs, check their outputs, and then remove all the bookkeeping files:

    bash cbmc-batch.sh -sec