Merge pull request #5457 from thomasspriggs/tas/gha_ancillaries

Port ancillary jobs from Travis to github actions

.github/workflows/pull-request-check-clang-format.sh

@@ -0,0 +1,38 @@
+#!/bin/bash
+
+# Stop on errors
+set -e
+
+# Log information about the run of this check.
+echo "Pull request's base branch is: ${BASE_BRANCH}"
+echo "Pull request's merge branch is: ${MERGE_BRANCH}"
+echo "Pull request's source branch is: ${GITHUB_HEAD_REF}"
+clang-format-7 --version
+
+# The checkout action leaves us in detatched head state. The following line
+# names the checked out commit, for simpler reference later.
+git checkout -b ${MERGE_BRANCH}
+
+# Build list of files to ignore 
+while read file ; do EXCLUDES+="':(top,exclude)$file' " ; done < .clang-format-ignore
+
+# Make sure we can refer to ${BASE_BRANCH} by name
+git checkout ${BASE_BRANCH}
+git checkout ${MERGE_BRANCH}
+
+# Find the commit on which the PR is based.
+MERGE_BASE=$(git merge-base ${BASE_BRANCH} ${MERGE_BRANCH})
+echo "Checking for formatting errors introduced since $MERGE_BASE"
+
+# Do the checking. "eval" is used so that quotes (as inserted into $EXCLUDES
+# above) are not interpreted as parts of file names.
+eval git-clang-format-7 --binary clang-format-7 $MERGE_BASE -- $EXCLUDES
+git diff > formatted.diff
+if [[ -s formatted.diff ]] ; then
+  echo 'Formatting error! The following diff shows the required changes'
+  echo 'Use the raw log to get a version of the diff that preserves spacing'
+  cat formatted.diff
+  exit 1
+fi
+echo 'No formatting errors found'
+exit 0

.github/workflows/pull-request-check-cpplint.sh

@@ -0,0 +1,24 @@
+#!/bin/bash
+
+# Stop on errors
+set -e
+
+# Log information about the run of this check.
+echo "Pull request's base branch is: ${BASE_BRANCH}"
+echo "Pull request's merge branch is: ${MERGE_BRANCH}"
+echo "Pull request's source branch is: ${GITHUB_HEAD_REF}"
+
+# The checkout action leaves us in detatched head state. The following line
+# names the checked out commit, for simpler reference later.
+git checkout -b ${MERGE_BRANCH}
+
+# Make sure we can refer to ${BASE_BRANCH} by name
+git checkout ${BASE_BRANCH}
+git checkout ${MERGE_BRANCH}
+
+# Find the commit on which the PR is based.
+MERGE_BASE=$(git merge-base ${BASE_BRANCH} ${MERGE_BRANCH})
+echo "Checking standards of code touched since $MERGE_BASE"
+
+# Do the checking.
+./scripts/run_diff.sh CPPLINT $MERGE_BASE

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

@@ -129,3 +129,50 @@ jobs:
 
       - name: Build cbmc
         run: "%SCRIPT_DIR%\\build-cbmc.bat"
+
+  check-clang-format:
+    runs-on: ubuntu-20.04
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: true
+          fetch-depth: 0
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get install -yq clang-format-7
+      - name: Check updated lines of code match clang-format-7 style
+        env:
+          BASE_BRANCH: ${{ github.base_ref }}
+          MERGE_BRANCH: ${{ github.ref }}
+        run: ./.github/workflows/pull-request-check-clang-format.sh
+
+  check-cpplint:
+    runs-on: ubuntu-20.04
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: true
+          fetch-depth: 0
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          pip install unidiff
+      - name: Check updated lines of code meet linting standards
+        env:
+          BASE_BRANCH: ${{ github.base_ref }}
+          MERGE_BRANCH: ${{ github.ref }}
+        run: ./.github/workflows/pull-request-check-cpplint.sh
+
+  check-string-table:
+    runs-on: ubuntu-20.04
+    steps:
+      - uses: actions/checkout@v2
+      - name: Check for unused irep ids
+        run: ./scripts/string_table_check.sh