Skip to content

Add empty struct support to incremental SMT decision procedure #6059

Add empty struct support to incremental SMT decision procedure

Add empty struct support to incremental SMT decision procedure #6059

name: Build Linux partially with CPROVER tools
on:
pull_request:
branches:
- '**'
jobs:
# This job takes approximately 18 minutes
CompileLinux:
runs-on: ubuntu-20.04
steps:
- uses: actions/checkout@v3
with:
submodules: true
- name: Install Packages
env:
# This is needed in addition to -yq to prevent apt-get from asking for
# user input
DEBIAN_FRONTEND: noninteractive
run: |
sudo apt-get update
sudo apt-get install --no-install-recommends -y clang-10 clang++-10 flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache
sudo apt-get install --no-install-recommends -y libssl-dev libelf-dev libudev-dev libpci-dev libiberty-dev autoconf
sudo apt-get install --no-install-recommends -y gawk jq
- name: Prepare ccache
uses: actions/cache@v3
with:
path: .ccache
key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-KERNEL
restore-keys: |
${{ runner.os }}-20.04-make-clang-${{ github.ref }}
${{ runner.os }}-20.04-make-clang
- name: ccache environment
run: |
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
- name: Zero ccache stats and limit in size
run: ccache -z --max-size=500M
- name: Build CBMC tools
run: |
make -C src minisat2-download
make -C src CXX='ccache /usr/bin/clang++' cbmc.dir goto-cc.dir goto-diff.dir -j2
- name: Print ccache stats
run: ccache -s
- name: Run (Docker Based) Linux Build test
run: integration/linux/compile_linux.sh
- uses: actions/upload-artifact@v3
with:
name: CPROVER-faultyInput
path: CPROVER/faultyInput/*