Add a Dockerfile github action.

This adds a github action that builds CBMC in a
Docker container, and then exercises a small suite
of smoke tests on it to make sure that the image
is sound.

Author: NlightNFotis

.github/workflows/pull-request-checks.yaml

@@ -349,3 +349,24 @@ jobs:
       - uses: actions/checkout@v2
       - name: Check for unused irep ids
         run: ./scripts/string_table_check.sh
+
+  check-docker-image:
+    runs-on: ubuntu-20.04
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: recursive
+      - name: Download test dependencies
+        run: sudo apt install openjdk-11-jdk-headless
+      - name: Build docker image
+        run: docker build -t cbmc .
+      - name: Smoke test goto-cc
+        run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc goto-cc -o /mnt/smoke/test.goto /mnt/smoke/test.c
+      - name: Smoke test cbmc
+        run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc cbmc /mnt/smoke/test.goto
+      - name: Smoke test jbmc
+        run: |
+          javac .github/workflows/smoke_test_assets/Test.java
+          docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc jbmc --classpath /mnt/smoke Test
+      - name: Smoke test goto-analyzer
+        run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc goto-analyzer /mnt/smoke/test.goto --unreachable-functions

.github/workflows/smoke_test_assets/Test.java

@@ -0,0 +1,6 @@
+public class Test {
+    public static void main(String[] args) {
+        System.out.println("Hi");
+        assert(1 == 1);
+    }
+}

.github/workflows/smoke_test_assets/test.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+#define return_val 0;
+
+int main(void)
+{
+  assert(1 == 1);
+  return return_val;
+}