Skip to content

Fix #779: Mark offset off as an integer constant #171

Fix #779: Mark offset off as an integer constant

Fix #779: Mark offset off as an integer constant #171

name: CN Spec Testing
on:
pull_request:
push:
branches:
- master
env:
CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release
# cancel in-progress job when a new push is performed
concurrency:
group: ci-${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
jobs:
build:
strategy:
matrix:
# version: [4.12.0, 4.14.1]
version: [4.14.1]
runs-on: ubuntu-22.04
steps:
- name: Checkout cerberus
uses: actions/checkout@v4
- name: System dependencies (ubuntu)
run: |
sudo apt-get install build-essential libgmp-dev z3 opam cmake lcov
- name: Restore cached opam
id: cache-opam-restore
uses: actions/cache/restore@v4
with:
path: ~/.opam
key: ${{ matrix.version }}
fail-on-cache-miss: true
- name: Install Cerberus
run: |
opam switch ${{ matrix.version }}
eval $(opam env --switch=${{ matrix.version }})
opam pin --yes --no-action add cerberus-lib .
opam pin --yes --no-action add cerberus .
opam install --yes cerberus
- name: Install CN
run: |
opam switch ${{ matrix.version }}
eval $(opam env --switch=${{ matrix.version }})
opam pin --yes --no-action add cn .
opam install --yes cn ocamlformat.0.26.2
- name: Run CN-runtime CI tests (Cerberus)
run: |
opam switch ${{ matrix.version }}
eval $(opam env --switch=${{ matrix.version }})
cd tests; ./run-cn-exec.sh
- name: Checkout cn-tutorial
uses: actions/checkout@v4
with:
repository: rems-project/cn-tutorial
path: cn-tutorial
ref: cn-runtime-testing # FIXME: remove once the branch is merged
- name: Run CN-runtime CI tests (CN tutorial)
run: |
opam switch ${{ matrix.version }}
eval $(opam env --switch=${{ matrix.version }})
cd cn-tutorial; ./runtime-test.sh
cd ..
- name: Run CN-Test-Gen CI tests
run: |
opam switch ${{ matrix.version }}
eval $(opam env --switch=${{ matrix.version }})
cd tests; ./run-cn-test-gen.sh