Skip to content

C library: Apple does not adhere to aarch64 ABI #9565

C library: Apple does not adhere to aarch64 ABI

C library: Apple does not adhere to aarch64 ABI #9565

name: Build Xen with CPROVER tools
on:
pull_request:
branches: [ develop ]
jobs:
# This job takes approximately 33 minutes
CompileXen:
runs-on: ubuntu-20.04
steps:
- uses: actions/checkout@v4
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 build-essential git flex bison software-properties-common curl python
sudo apt-get install --no-install-recommends -y bin86 gdb bcc liblzma-dev python-dev gettext iasl uuid-dev libncurses5-dev libncursesw5-dev pkg-config
sudo apt-get install --no-install-recommends -y libgtk2.0-dev libyajl-dev time ccache clang-10 clang++-10
- name: Prepare ccache
uses: actions/cache@v4
with:
save-always: true
path: .ccache
key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-XEN
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 -j4
- name: Print ccache stats
run: ccache -s
- name: Get one-line-scan
run: git clone -b path-addition https://github.com/awslabs/one-line-scan.git
- name: Get Xen 4.13
run: git clone git://xenbits.xen.org/xen.git xen_4_13 && cd xen_4_13 && git reset --hard RELEASE-4.13.0 && pwd
- name: Prepare compile Xen with CBMC via one-line-scan
run: |
ln -s goto-cc src/goto-cc/goto-ld
ln -s goto-cc src/goto-cc/goto-as
ln -s goto-cc src/goto-cc/goto-g++
- name: Compile Xen with CBMC via one-line-scan, and check for goto-cc section
run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 4 -- make -C xen_4_13 xen -j $(nproc)
- name: Check for goto-cc section in xen-syms binary
run: objdump -h xen_4_13/xen/xen-syms | grep "goto-cc"
- name: Show goto-cc properties
run: $(pwd)/src/cbmc/cbmc --show-properties xen_4_13/xen/xen-syms
- name: Show some goto-cc functions
run: $(pwd)/src/cbmc/cbmc --list-goto-functions xen_4_13/xen/xen-syms | grep "arch"