xen-cbmc: fix ci script #5508
xen-cbmc: fix ci script #5508
Conversation
nmanthey
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
There was a problem hiding this comment.
Thanks for the fix! I would say it's much needed 👍
May I ask why the file was renamed from .yml to .yaml? This has the unfortunate side effect of breaking file revision history, which makes it hard to detect what the actual change here is (the one that actually fixed the broken CI issue).
| 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 3 -- make -C xen_4_13 xen -j $(nproc) -k || true |
There was a problem hiding this comment.
Could you split this over multiple lines? This is a bit hard to read.
Rename the file for consistency with the other files in this directory. Signed-off-by: Norbert Manthey <nmanthey@amazon.de>
I will split the commit into (1) file rename, and (2) actual diff. The rename is basically for consistency. Yes, I can split that over multiple lines. Yes, this fix should stop those PR emails (I hope, I did not push PRs recently ;) ) |
nmanthey
force-pushed
the
cbmc-xen-ci
branch
from
3ca634b to
3aecb5d
Compare
This script has been broken, and not been picked up in CI until now. This change fixes the script, as well as makes sure that the relevant steps are executed, and the resulting build artefacts have the required goto-cc section in them. This CI script has been refered to as part of the paper: "Using model checking tools to triage the severity of security bugs in the Xen hypervisor", that has been presented at FMCAD 2020. Signed-off-by: Norbert Manthey <nmanthey@amazon.de>
nmanthey
force-pushed
the
cbmc-xen-ci
branch
from
3aecb5d to
20680de
Compare
Codecov Report
@@ Coverage Diff @@
## develop #5508 +/- ##
========================================
Coverage 68.34% 68.34%
========================================
Files 1187 1187
Lines 98090 98090
========================================
Hits 67044 67044
Misses 31046 31046
Flags with carried forward coverage won't be shown. Click here to find out more. Continue to review full report at Codecov.
|
This script has been broken, and not been picked up in CI until now.
This change fixes the script, as well as makes sure that the relevant
steps are executed, and the resulting build artefacts have the required
goto-cc section in them.
This CI script has been refered to as part of the paper:
"Using model checking tools to triage the severity of security bugs in
the Xen hypervisor", that has been presented at FMCAD 2020.
Signed-off-by: Norbert Manthey nmanthey@amazon.de