From 63237ae6e1c427228d28425682c06be3bc2b0d16 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Mon, 7 Sep 2020 21:06:38 +0200 Subject: [PATCH 1/3] cbmc: test compile Xen In the past, changes to CPROVER tools resulted in a broken build for systems software like e.g. Xen. To avoid this issue in the future, we want to integrate Xen compilation into continuous testing. This allows to identify issues early, and fix them appropriately. Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yml | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/.github/workflows/build-and-test-Xen.yml b/.github/workflows/build-and-test-Xen.yml index 7aab6780232..f52a3e7a5c4 100644 --- a/.github/workflows/build-and-test-Xen.yml +++ b/.github/workflows/build-and-test-Xen.yml @@ -22,5 +22,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 From 6f13454b5d4eb4b5904667d61d8fc325e954525f Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 8 Sep 2020 11:17:36 +0200 Subject: [PATCH 2/3] workflows: check xen on PR Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/build-and-test-Xen.yml b/.github/workflows/build-and-test-Xen.yml index f52a3e7a5c4..39f51a31117 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: From 27c7dffa44847f51ccca05e252590b647e662201 Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Tue, 8 Sep 2020 11:23:44 +0200 Subject: [PATCH 3/3] workflow: touch nit Signed-off-by: Norbert Manthey --- .github/workflows/build-and-test-Xen.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/build-and-test-Xen.yml b/.github/workflows/build-and-test-Xen.yml index 39f51a31117..ce19353ffe0 100644 --- a/.github/workflows/build-and-test-Xen.yml +++ b/.github/workflows/build-and-test-Xen.yml @@ -16,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