Skip to content

Attempt to invoke CN jobs with one-line scripts #7

Attempt to invoke CN jobs with one-line scripts

Attempt to invoke CN jobs with one-line scripts #7

Workflow file for this run

# This is a basic workflow to help you get started with Actions
name: Code Verification
# Controls when the workflow will run
on:
# Triggers the workflow on push or pull request events but only for the develop branch
push:
# Allows you to run this workflow manually from the Actions tab
#workflow_dispatch:
# A workflow run is made up of one or more jobs that can run sequentially or in parallel
jobs:
mps-verify-cn:
runs-on: ubuntu-latest
steps:
- name: Checkout repository and submodules
uses: actions/checkout@v4
- name: Prove MPS Components
uses: tj-actions/docker-run@v2
with:
image: podhrmic/cerberus:release
name: cerberus
options: -v ${{ github.workspace }}:/data
# This action seems to override the docker image entrypoint, as a result
# we need to run "eval `opam env`" first
# Use `>` so newlines will be replaced with spaces
args: >
eval `opam env` &&
cd components/mission_protection_system/src &&
make -f cn.mk proofs
mps-verify-frama-c:
runs-on: ubuntu-latest
steps:
- name: Checkout repository and submodules
uses: actions/checkout@v4
- name: Prove MPS Components
uses: tj-actions/docker-run@v2
with:
image: framac/frama-c:dev
name: framac
options: -v ${{ github.workspace }}:/work -w /work
args: >
cd components/mission_protection_system/src &&
mkdir -p wp-session/script &&
mkdir -p wp-session/cache &&
make -f frama_c.mk proofs