Add ctags unit test to github workflow

Author: Mark R. Tuttle

.github/workflows/ctags.yaml

@@ -0,0 +1,92 @@
+name: Test generating symbols from ctags
+on:
+  pull_request:
+    types: [opened, synchronize, reopened, labeled, unlabeled]
+
+jobs:
+  legacy:
+    name: Legacy ctags test
+    runs-on: macos-latest
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+      - name: Install viewer
+        run: |
+          make install
+      - name: Install brew packages
+        run: |
+          brew uninstall ctags || true
+          brew uninstall universal-ctags || true
+          brew install cbmc cbmc-starter-kit litani
+      - name: Build goto
+        run: |
+          cd tests/unit-tests/ctags
+          make clone
+          pushd coreHTTP/test/cbmc
+          cbmc-starter-kit-update --remove-litani --remove-starter
+          popd
+          make build
+      - name: Test legacy ctags
+        run: |
+          cd tests/unit-tests/ctags
+          ctags || true
+          make legacy
+
+  exuberant:
+    name: Exuberant ctags test
+    runs-on: macos-latest
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+      - name: Install viewer
+        run: |
+          make install
+      - name: Install brew packages
+        run: |
+          brew uninstall ctags || true
+          brew uninstall universal-ctags || true
+          brew install cbmc cbmc-starter-kit litani ctags
+      - name: Build goto
+        run: |
+          cd tests/unit-tests/ctags
+          make clone
+          pushd coreHTTP/test/cbmc
+          cbmc-starter-kit-update --remove-litani --remove-starter
+          popd
+          make build
+      - name: Run exuberant ctags test
+        run: |
+          cd tests/unit-tests/ctags
+          ctags --version
+          make exuberant
+
+  universal:
+    name: Universal ctags test
+    runs-on: macos-latest
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+      - name: Install viewer
+        run: |
+          make install
+      - name: Install brew packages
+        run: |
+          brew uninstall ctags || true
+          brew uninstall universal-ctags || true
+          brew install cbmc cbmc-starter-kit litani universal-ctags
+      - name: Build goto
+        run: |
+          cd tests/unit-tests/ctags
+          make clone
+          pushd coreHTTP/test/cbmc
+          cbmc-starter-kit-update --remove-litani --remove-starter
+          popd
+          make build
+      - name: Run universal ctags test
+        run: |
+          cd tests/unit-tests/ctags
+          ctags --version
+          make universal

tests/unit-tests/ctags/.gitignore

@@ -0,0 +1,2 @@
+coreHTTP
+symbol.json

tests/unit-tests/ctags/Makefile

@@ -0,0 +1,47 @@
+# The FreeRTOS coreHTTP respository
+REPO_DIR = coreHTTP
+REPO_URL = https://github.com/FreeRTOS/coreHTTP.git
+
+# Paths in the repository
+PROOF_DIR = test/cbmc/proofs
+
+# Proofs in the repository
+PROOF = HTTPClient_AddRangeHeader
+
+UNIVERSAL=$$(ctags --version | grep Universal)
+EXUBERANT=$$(ctags --version | grep Exuberant)
+
+default: clone build compare
+
+# Clone the repository
+clone:
+	$(RM) -r $(REPO_DIR)
+	git clone $(REPO_URL) $(REPO_DIR)
+	cd $(REPO_DIR); git submodule update --init --checkout --recursive
+
+# Run a proofs
+#   EXTERNAL_SAT_SOLVER= to ensure cbmc uses minisat and not kissat
+build:
+	cd $(REPO_DIR)/$(PROOF_DIR)/$(PROOF); \
+	    EXTERNAL_SAT_SOLVER= \
+	    make goto
+
+symbol:
+	cbmc-viewer symbol \
+		--goto $(REPO_DIR)/$(PROOF_DIR)/$(PROOF)/gotos/$(PROOF)_harness.goto \
+		--srcdir $(REPO_DIR) > symbol.json
+
+legacy: symbol
+	diff symbol.json symbol-legacy.json
+
+exuberant: symbol
+	diff symbol.json symbol-exuberant.json
+
+universal: symbol
+	diff symbol.json symbol-universal.json
+
+clean:
+	$(RM) *~ symbol.json
+
+veryclean: clean
+	$(RM) -r $(REPO_DIR)