Skip to content

gh: finishing publication fixes #6

gh: finishing publication fixes

gh: finishing publication fixes #6

Workflow file for this run

name: Sentry kernel proof
on:
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: 'mesonbuild/ubuntu-rolling'
steps:
- name: install prerequisites pkg
uses: outpost-os/action-install-pkg@v1
with:
packages: 'dtc|device-tree-compiler,curl,lld,opam,why3,graphviz,libgmp-dev,libgtksourceview-3.0-dev'
- name: install frama-C
run: |
opam init --compiler 4.14.1 --disable-sandboxing --yes --confirm-level=yes
eval $(opam env)
opam install --yes --confirm-level=yes frama-c
- 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
- name: checkout repo
uses: actions/checkout@v4
with:
ref: ${{ github.ref }}
fetch-depth: 0
set-safe-directory: '*'
- name: Install local deps
run: |
pip3 install -r requirements.txt
- name: defconfig
run: |
defconfig configs/nucleo_u5a5_autotest_defconfig
- 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.dts -Ddts-include-dirs=dts -Dwith_proof=true'
- name: run framaC
run: |
why3 config detect
frama-c -wp-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