stefadp/juliet-c repository overview

⁠juliet-test-suite

Creating environments to deal with the Juliet Test Suite for C v1.3. The image automatically builds the test cases using make to generate.

The WORKING DIRECTORY is /juliet/c

⁠How to use

docker pull stefadp/juliet-c:latest

To use the files from other repositories, you can simply create a shared volume on your host and copy there the folders and files present in /juliet/c/C/src, namely testcases and testcasesupport

For example, consider the situation in which someone wants to analyze the performance of a static analysis tool such as CBMC⁠ on the Juliet Test Suite. A container can exists containing all the dependencies and programs to run the tool. In this example we use the stefadp/cbmc⁠ as image for the container.

⁠Create a shared volume on the host machine

First

docker pull stefadp/juliet-c:latest

then open your terminal and create a folder to share among containers:

sudo mkdir <path-to-desired-location>/hostvolume

Next, launch a container named juliet-test and map /hostvolume on the host to a volume on the container with the command:

sudo docker run -it --name juliet-test -v <path-to-desired-location>/hostvolume:/shared stefadp/juliet-c:latest

In this case we created a folder /shared as volume on the container. That folder does not exists in the container and is automatically generated when running the command above.

Once you are at the new container's command prompt, move to root folder with: cd /

You can now copy the test cases (or a set of them) to the shared volume with the command:

cp -a /juliet/c/C/src/. /shared

Detach from the container with Ctrl-p + Ctrl-q and return to the host machine's command prompt. Once there, list the files in the shared volume (/hostvolume) with the command:

sudo ls <path-to-desired-location>/hostvolume

You will see the folders we copied from the container.

⁠Running cbmc on the files in the shared volume

First run

docker pull stefadp/cbmc:latest

Next, launch a container named jbmc-test and map /hostvolume on the host to a volume on the container with the command:

sudo docker run -it --name juliet-test -v <path-to-desired-location>/hostvolume:/shared stefadp/juliet-c:latest

In this case we created a folder /shared as volume on the container (note: the name can differ from the /shared in the previous container) . That folder does not exists in the container and is automatically generated when running the command above.

Once you are at the new container's command prompt, list the files in the shared volume with the command:

ls /shared

You will see the test cases which we copied on the host in the previous steps.

You can now use use cbmc on the test cases with:

cbmc file.c [OPTIONS]

and store the results in the shared volume, with:

mkdir /shared/results

``````cbmc file.c [OPTIONS] >> /shared/results/results.txt```

They will automatically being copied on the host machine.