From 0696d589b97b8b655ffb5b93b0078a2a033841be Mon Sep 17 00:00:00 2001 From: Soren Ptak Date: Fri, 15 Dec 2023 14:40:41 -0500 Subject: [PATCH] Change the ci.yml file to use the paid runner when running from FreeRTOS, and use a free ubuntu-20.04 runner if run from a users fork --- .github/workflows/ci.yml | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b1105ae..f12c456 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -198,8 +198,8 @@ jobs: config: .github/memory_statistics_config.json check_against: docs/doxygen/include/size_table.md - proof_ci: - if: ${{ github.event.pull_request }} + proof_ci_cbmc_runner: + if: ${{ github.event.repository.owner }} == "FreeRTOS" runs-on: cbmc_ubuntu-latest_16-core steps: - name: Set up CBMC runner @@ -211,3 +211,17 @@ jobs: uses: FreeRTOS/CI-CD-Github-Actions/run_cbmc@main with: proofs_dir: test/cbmc/proofs + + proof_ci_ubuntu_runner: + if: ${{ github.event.repository.owner }} != "FreeRTOS" + runs-on: ubuntu-20.04 + steps: + - name: Set up CBMC runner + uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main + with: + cbmc_version: "5.61.0" + cbmc_viewer_version: "3.5" + - name: Run CBMC + uses: FreeRTOS/CI-CD-Github-Actions/run_cbmc@main + with: + proofs_dir: test/cbmc/proofs