diff --git a/.github/workflows/build-and-test-Xen.yml b/.github/workflows/build-and-test-Xen.yml index 7aab6780232..ce19353ffe0 100644 --- a/.github/workflows/build-and-test-Xen.yml +++ b/.github/workflows/build-and-test-Xen.yml @@ -1,6 +1,8 @@ name: Build and Test Xen -on: [push] +on: + pull_request: + branches: [ develop ] jobs: Linux: @@ -14,7 +16,8 @@ jobs: software-properties-common libwww-perl python \ bin86 gdb bcc liblzma-dev python-dev gettext iasl \ uuid-dev libncurses5-dev libncursesw5-dev pkg-config \ - libgtk2.0-dev libyajl-dev sudo time + libgtk2.0-dev libyajl-dev sudo \ + time - uses: actions/checkout@v1 @@ -22,5 +25,17 @@ jobs: run: make -C src minisat2-download run: make -C src cbmc.dir goto-cc.dir goto-diff.dir + - name: get one-line-scan + run: git clone 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 + + - name: compile Xen with CBMC via one-line-scan + run: ls + run: pwd + run: ls src/* + run: ln -sf src/goto-cc/goto-cc src/goto-cc/goto-ld + run: ln -sf src/goto-cc/goto-cc src/goto-cc/goto-as + run: ln -sf src/goto-cc/goto-cc src/goto-cc/goto-g++ + run: PATH=$PATH:src/cbmc:src/goto-cc one-line-scan/one-line-scan --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen xen -j $(nproc) -k