Skip to content

Removing from repo. Will add new MSP (which is rename of RGS) and Op… #16

Removing from repo. Will add new MSP (which is rename of RGS) and Op…

Removing from repo. Will add new MSP (which is rename of RGS) and Op… #16

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: addnab/docker-run-action@v3
with:
image: podhrmic/cerberus:release
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
run: >
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: addnab/docker-run-action@v3
with:
image: framac/frama-c:dev
options: -v ${{ github.workspace }}:/work -w /work
run: |
cd components/mission_protection_system/src
mkdir -p /tmp/wp-session/script
mkdir -p /tmp/wp-session/cache
make -f frama_c.mk proofs