Skip to content

Added equivalence checking extensions #602

Added equivalence checking extensions

Added equivalence checking extensions #602

Workflow file for this run

name: SMACK CI
on: [push, pull_request]
jobs:
check-regressions:
runs-on: ubuntu-20.04
strategy:
matrix:
regtest_env:
[
"--exhaustive --folder=c/basic",
"--exhaustive --folder=c/data",
"--exhaustive --folder=c/ntdrivers-simplified",
"--exhaustive --folder=c/ntdrivers",
"--exhaustive --folder=c/bits",
"--exhaustive --folder=c/float",
"--exhaustive --folder=c/locks",
"--exhaustive --folder=c/contracts",
"--exhaustive --folder=c/simd",
"--exhaustive --folder=c/memory-safety",
"--exhaustive --folder=c/pthread",
"--exhaustive --folder=c/pthread_extras",
"--exhaustive --folder=c/strings",
"--exhaustive --folder=c/special",
"--exhaustive --folder=c/targeted-checks",
"--exhaustive --folder=c/unroll",
"--exhaustive --folder=rust/array --languages=rust",
"--exhaustive --folder=rust/basic --languages=rust",
"--exhaustive --folder=rust/box --languages=rust",
"--exhaustive --folder=rust/functions --languages=rust",
"--exhaustive --folder=rust/generics --languages=rust",
"--exhaustive --folder=rust/loops --languages=rust",
"--exhaustive --folder=rust/panic --languages=rust",
"--exhaustive --folder=rust/recursion --languages=rust",
"--exhaustive --folder=rust/structures --languages=rust",
"--exhaustive --folder=rust/targeted-checks",
"--exhaustive --folder=rust/vector --languages=rust",
"--exhaustive --folder=rust/cargo/** --languages=cargo --threads=1",
"--exhaustive --folder=llvm --languages=llvm-ir"
]
steps:
- uses: actions/checkout@v2
- name: install dependencies
env:
GITHUB_ACTIONS: true
run: INSTALL_DEV_DEPENDENCIES=1 INSTALL_RUST=1 ./bin/build.sh
- name: format checking
run: |
./format/run-clang-format.py -r lib/smack include/smack tools share/smack/include share/smack/lib test examples
flake8 test/regtest.py share/smack/ --extend-exclude share/smack/svcomp/,share/smack/reach.py
- name: compile and test
env:
REGTEST_ENV: ${{ matrix.regtest_env }}
run: ./bin/build.sh
build-and-push-docker:
runs-on: ubuntu-20.04
needs: check-regressions
steps:
- name: Check Out Repo
uses: actions/checkout@v2
- name: Login to Docker Hub
uses: docker/login-action@v1
with:
username: ${{ secrets.DOCKER_HUB_USERNAME }}
password: ${{ secrets.DOCKER_HUB_ACCESS_TOKEN }}
- name: Set up Docker Buildx
id: buildx
uses: docker/setup-buildx-action@v1
# borrowed from:
# https://stackoverflow.com/questions/58033366/how-to-get-current-branch-within-github-actions/58035262
- name: Extract branch name
shell: bash
run: echo "##[set-output name=branch;]$(echo ${GITHUB_REF#refs/heads/})"
id: extract_branch
- name: Set tag name
shell: bash
id: set_tag
run: |
if [ ${{ steps.extract_branch.outputs.branch }} == 'master' ]; then echo "##[set-output name=docker_tag;]$(echo stable)" && exit 0; fi
if [ ${{ steps.extract_branch.outputs.branch }} == 'develop' ]; then echo "##[set-output name=docker_tag;]$(echo latest)" && exit 0; fi
echo "##[set-output name=docker_tag;]$(echo none)"
- name: Build and push
if: ${{ steps.set_tag.outputs.docker_tag != 'none' }}
id: docker_build
uses: docker/build-push-action@v2
with:
context: ./
file: ./Dockerfile
push: true
tags: smackers/smack:${{ steps.set_tag.outputs.docker_tag }}
- name: Image digest
run: echo ${{ steps.docker_build.outputs.digest }}