Update CI (after merges?)
Small things to fix next time we update CI.
Random job failures:
-
unit-tests:jdk-17: one flapping timeout -
checkstyle: Unable to create Root Module
-
Host more images, so we do not pull images from docker multiple times for each pipeline. We (this instance of GitLab) reach Docker's limit sometimes (e.g. this job). The used images are -
a few python images for a few checks and generating regression tests' pipeline (these run every pipeline) -
kaniko for our images (run rarely and only manually) -
reuse for the license check (but it didn't fail last time) -
any I missed?
-
-
Avoid check if jar is uptodate (e.g. these jobs for some reason) -
But in general, do not ignore when BenchExec fails
-
Configurations:
-
Configure which functions without bodies are safe. (or turn STRICT
toASSUME_SAFE
for-smg
). -
Some tests should be changed to reachsafety
, e.g. these have shown regression not because SMG found an error, but because a function call without function body was reached.- or maybe just fix function without bodies and ignore reachsafety.
- or maybe use another specification including both memsafety and reachsafety (maybe termination too? see
.spc
files anyway).
-
Ignore original file lines in drivers, so logs don't look like this. Use parser.readLineDirectives=false
. -
Fix output: Warning: Could not write information about the error path to file /builds/verification/cpachecker/output (Read-only file system)
.
Test suits:
-
#27 check and fix LDV-benchmarks -
#34 fix test/programs/smg_External_Allocation_Test
-
use other tests: smg_Explicity_Test
,smg_External_Allocation_Test
,smg_options_test
,smg_predicates
,smgListAbstraction
-
#39 add predicate/reachability tests in CI
Miscellaneous:
-
Disallow failure for bigger
regression tests, so they either block pipeline, or are run. (Now it shows warnings instead of failures, which can be confusing.) -
Store .xml
files instead of.xml.bz2
archives, so their diffs are human-readable and meaningful when updating results. -
Rename stages in regression tests or, better, restructure them so bigger
is not a few screens long. -
Fix improvements count (e.g. this job). Closed in !17 (merged) -
see #20? -
Zip regression job's output.xml so it's easy to download it from the job's artifacts. Closed in !17 (merged)
Edited by Петров Олег Максимович