summaryrefslogtreecommitdiff
path: root/.github
diff options
context:
space:
mode:
authorKareem Khazem <karkhaz@karkhaz.com>2023-03-03 22:35:42 +0000
committerGitHub <noreply@github.com>2023-03-03 14:35:42 -0800
commit408c3841eacad990110631194d8aa73786d2e685 (patch)
tree558e1d2fee224501d166b203f67f0e72dcee41fc /.github
parent9fa0fb7f0d82086035ccfdd4bec73a16c41f9d48 (diff)
downloadfreertos-git-408c3841eacad990110631194d8aa73786d2e685.tar.gz
Add CBMC proof-running GitHub Action (#924)
This commit adds a GitHub Action that runs the CBMC proofs upon every push and pull request. This is intended to replace the current CBMC CI.
Diffstat (limited to '.github')
-rw-r--r--.github/workflows/ci.yml18
1 files changed, 14 insertions, 4 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 24e630380..5887c1172 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -172,7 +172,17 @@ jobs:
path: ./freertos_lts_memory_estimates.json
retention-days: 2
-
-
-
-
+ proof_ci:
+ runs-on: cbmc_ubuntu-latest_16-core
+ steps:
+ - uses: actions/checkout@v2
+ - run: |
+ git submodule update --init --checkout --recursive --depth 1
+ sudo apt-get update
+ sudo apt-get install --yes --no-install-recommends gcc-multilib
+ - name: Set up CBMC runner
+ uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main
+ - name: Run CBMC
+ uses: FreeRTOS/CI-CD-Github-Actions/run_cbmc@main
+ with:
+ proofs_dir: FreeRTOS/Test/CBMC/proofs