linuxci: test compiling linux #5
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
added 5 commits
March 10, 2021 20:08
nmanthey
force-pushed
the
linux-github-ci
branch
from
9c08504 to
4fe2b96
Compare
Codecov Report
@@ Coverage Diff @@
## develop #5 +/- ##
==========================================
Coverage ? 75.02%
==========================================
Files ? 1431
Lines ? 155295
Branches ? 0
==========================================
Hits ? 116504
Misses ? 38791
Partials ? 0 Continue to review full report at Codecov.
|
nmanthey
force-pushed
the
linux-github-ci
branch
from
4fe2b96 to
a568669
Compare
nmanthey
force-pushed
the
linux-github-ci
branch
4 times, most recently
from
a852e84 to
254acbd
Compare
Moving them to cbmc-cpp as they test VERIFICATION results, with few exceptions that were safe to be placed in the cpp folder. Adding `#include <cassert>` as needed.
nmanthey
force-pushed
the
linux-github-ci
branch
3 times, most recently
from
38e59d2 to
ffc036a
Compare
Enable cpp-from-CVS regression tests
As part of the regular release process.
Increase version number to 5.26.0
nmanthey
force-pushed
the
linux-github-ci
branch
3 times, most recently
from
8c88986 to
b16829e
Compare
…n-reg-tests Adds code contracts regression tests that involve function calls
Commit 879afa2 introduced tests that result in name conflicts on non-case-sensitive file systems. Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Properly rename regression tests from cbmc-cpp
We have these tests in the repository, but did not include them in either Makefile or CMake configurations. They can't work right now as the "--incremental" command-line option doesn't yet exist, thus marking them as "FUTURE."
For as long as goto-programs/ uses util/c_types.h, expression types generated during goto-program construction rely on bit widths to be configured.
The Python script silently failed when invoked from run_diff.sh, which redirects stdout to a file, when unidiff was not available.
Using Python 3 (as is the default GitHub's Ubuntu 20.04) requires merging changes from https://github.com/cpplint/cpplint, which is a larger undertaking.
This check cannot be disabled.
We have regression tests for cpplint.py, and should perhaps have used them to avoid silently failing.
…ests Add cbmc --incremental regression tests as FUTURE
The `__CPROVER_loop_invariant` contract used to incorrectly havoc the underlying pointer location instead of just havocing the value at the memory location. This commit fixes this.
Store the elements to be removed in a set until after the iteration is done, and then remove the chosen elements. The more standard approach could be returning the iterator to the next element in the remove-an-element function, but this requires larger changes here. Thus keeping it small and simple for now.
These regression tests are a selected subset (cf. README.txt) of the full set of available tests (stored in goto-instrument-wmm-full.tgz), and will ensure basic testing of the functionality implemented in goto-instrument. Test specifications were updated to work with current infrastructure.
Make all regression tests from the archive available (yet marking them as
THOROUGH or KNOWNBUG to avoid including them by default). This avoids having an
unused archive file bit-rotting in the repository. This commit was generated as
follows:
```
set -e
cd regression/goto-instrument-wmm-core/
tar xzf ../goto-instrument-wmm-full.tgz --strip-components=1
for f in $(tar tzf ../goto-instrument-wmm-full.tgz | sed 's#^goto-instrument-wmm-full/##')
do
[ -f $f ] || continue
if git status --porcelain $f | grep -q '^?'
then
if [[ $(basename $f) == "test.desc" ]]
then
sed -i '1s/^CORE$/THOROUGH/' $f
if ! grep -q EXIT $f
then
if grep -q "VERIFICATION FAILED" $f
then
sed -i '/SIGNAL=0/ i ^EXIT=10$' $f
else
sed -i '/SIGNAL=0/ i ^EXIT=0$' $f
fi
fi
elif [[ $f =~ \.c$ ]]
then
clang-format -i $f
fi
git add $f
else
git checkout -- $f
fi
done
git rm ../goto-instrument-wmm-full.tgz
git commit -F - <<EOF
Add regression tests from goto-instrument-wmm-full.tgz
Make all regression tests from the archive available (yet marking them as
THOROUGH or KNOWNBUG to avoid including them by default). This avoids having an
unused archive file bit-rotting in the repository. This commit was generated as
follows:
\`\`\`
$(<../../script.sh)
\`\`\`
EOF
```
Tag all *_OPT tests "glpk" and exclude them from test runs by default as we don't currently build with glpk by default.
Some of the tests that were previously imported as THOROUGH from the tar archive actually are failing and require further investigation.
These tests currently pass and each of them completes in under 1 second.
symtab2gb should populate configt
Make cpplint check actually work in CI
Enable regression tests of weak memory model instrumentation
nmanthey
force-pushed
the
linux-github-ci
branch
from
ce923f1 to
d882190
Compare
Script the steps required to build linux, so that they can also be executed locally. Signed-off-by: Norbert Manthey <nmanthey@amazon.de> Signed-off-by: Norbert Manthey <nmanthey@amazon.de>
Similarly to Xen, CBMC should be able to compile the linux kernel. As compiling the full kernel is very time consuming, and with CBMC also space consuming, only compile a core part all its dependencies, with the smalles configuration possible. For this core part, we select the KVM hypervisor. Once this is working, the configuration, as well as targets to be compiled can be increased. When the linuxci fails, we want to be able to easily understand the failure. The used one-line-scan tool already captures input files that cannot be handled by goto-cc. Hence, also archives these files for easy access in the web UI. Signed-off-by: Norbert Manthey <nmanthey@amazon.de>
nmanthey
force-pushed
the
linux-github-ci
branch
from
d882190 to
35d395e
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Similarly to Xen, CBMC should be able to compile the linux kernel. As
compiling the full kernel is very time consuming, and with CBMC also
space consuming, only compile a single file and all its dependencies,
with the smalles configuration possible.
Once this is working, the configuration, as well as targets to be
compiled can be increased.
Signed-off-by: Norbert Manthey nmanthey@amazon.de