proof.yml

name: Sentry kernel proof with Frama-C

on:
  push:
  pull_request:
    branches:
    - main

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true


jobs:
  run_framac:
    defaults:
      run:
        shell: bash
    runs-on: ${{ vars.DEFAULT_RUNNER_NAME }}
    container: 'pthierry38/framac-runner:29'
    timeout-minutes: 60
    steps:
      - uses: actions/checkout@v4
        with:
          fetch-depth: 0
          fetch-tags: true
          set-safe-directory: true
      - name: install prerequisites pkg
        uses: outpost-os/action-install-pkg@v1
        with:
          packages: 'device-tree-compiler,curl,lld,graphviz,lsb-release,libglib2.0-dev-bin,python3,python3-pip,python3-venv'
      - name: Spawn and use python venv
        run: |
          python3 -m venv venv
          echo "$PWD/venv/bin" >> $GITHUB_PATH
      - name: Clone cross-files
        uses: actions/checkout@v4
        with:
          ref:  'main'
          repository: 'outpost-os/meson-cross-files'
          path: crossfiles
      - name: Deploy cross-files
        run: |
          mkdir -p $HOME/.local/share/meson/cross
          cp -a $GITHUB_WORKSPACE/crossfiles/*.ini $HOME/.local/share/meson/cross
          echo "MESON_CROSS_FILES=$HOME/.local/share/meson/cross" >> $GITHUB_ENV
        shell: bash
      - name: Setup Rust toolchain
        uses: dtolnay/rust-toolchain@v1
        with:
          toolchain: nightly
          targets: thumbv7m-none-eabi,thumbv7em-none-eabi,thumbv7em-none-eabihf
          components: clippy,rustfmt
      - name: Setup C toolchain
        uses: outpost-os/action-setup-compiler@v1
        with:
          compiler: gcc
          triple: arm-none-eabi
          workspace: $GITHUB_WORKSPACE
      - name: Install local deps
        run: |
          pip3 install -r requirements.txt
      - name: defconfig
        run: |
          defconfig configs/nucleo_u5a5_autotest_defconfig
      - name: set safe dir for dunami (to be removed)
        run: |
          git config --global --add safe.directory '*'
        shell: bash
      - name: Meson Build
        uses: outpost-os/action-meson@main
        with:
          cross_files: ${{ format('{0}/{1}', env.MESON_CROSS_FILES, 'arm-none-eabi-gcc.ini') }}
          actions: '["prefetch", "setup"]'
          options: '-Dconfig=.config -Ddts=dts/examples/nucleo_u5a5_autotest.dts -Ddts-include-dirs=dts -Dwith_proof=true'
      - name: run framaC
        run: |
          why3 config detect
          cd builddir && meson test --suite proof
      - name: Meson postcheck
        if: failure()
        run: |
          cat builddir/meson-logs/meson-log.txt || true
          cat builddir/meson-logs/testlog.txt || true