1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
# 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 --start
You can then check CBMC Batch results locally by running
bash cbmc-batch.sh --end
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 --cleanup
|
