Errors in CI
The following errors are present in the integration tests, see log.csv pipeline artifact or gitlab-ci/*.csv files. I list them here for completeness. Maybe we should close this issue after each error is fixed, moved in a separate issue, or marked as "won't fix".
- wrong verdict
- inconsistent SMG (runtime check failed). test/programs/benchmarks/memsafety-ext/tree_cnstr.i and test/programs/benchmarks/memsafety-ext/tree_dsw.i can fail on different states.
- NullPointerException (test/programs/benchmarks/array-memsafety/cstrchr_unsafe.i)
- *Unsupported feature (recursion) — maybe we should adjust settings or disable these tests
- Unhandled realloc function (test/programs/benchmarks/array-memsafety-realloc/array-realloc-1.i, -2.i, -3.i)
- *
-smg
terminates with error on most tests from arrays (not included in CI). I'm not sure if analysis should fail with error when it cannot evaluate explicit address or just returnUnknown
. - *Unsupported feature (atexit) — see also LMU issue 803
- Unrecognized C code (More Initializers in initializer list ... than fit in type ...) — test/programs/benchmarks/ldv-memsafety/memleaks_test23_1.i, 23_2.i
- Unknown function '...' may be unsafe — adjust settings?
- DUPFFexgcd — test/programs/benchmarks/memsafety/20020406-1.i
- __assert_fail — test/programs/benchmarks/list-ext-properties/list-ext.i and other
- is_list_containing_x — test/programs/benchmarks/heap-manipulation/dancing.i
- dll_create_generic — test/programs/benchmarks/heap-manipulation/dll_of_dll-1.i
- alloca — test/programs/benchmarks/memsafety-ext3/freeAlloca.c, test/programs/benchmarks/memsafety-ext3/getNumbers1-1.c
- Unsupported feature (Not able to compute allocation size) — test/programs/benchmarks/ldv-memsafety/memleaks_test17_2-2.i and other
- Unrecognized C code (SMG cannot be evaluated): list->next — test/programs/benchmarks/heap-manipulation/sll_to_dll_rev-2.i
- Unrecognized C code (Could not resolve type.): char str1[MAX]; — test/programs/benchmarks/loops/invert_string-2.c
- Unsupported feature (pthread_create) — test/programs/benchmarks/pthread-memsafety/fillarray.i, 1.i, and test/programs/benchmarks/pthread-memsafety/list1.i [note: first two are a 'Not able to compute allocation size' for
-smg
]
drivers:
- Parsing failed (ProblemType) — test/programs/ldv-benchmarks/linux-5.10.120-memsafety/unknown/drivers---net---ethernet---marvell---mvpp2---mvpp2.ko.i
- Parsing failed (Syntax error) — test/programs/ldv-benchmarks/linux-5.10.120-memsafety/unknown/drivers---net---virtio_net.ko.i
* We discussed with @vasilyev that in these cases for real world programs we want to traverse other paths (maybe we can find an error there). For tests/competitions, we want to fail to notice bad input, as far as I understand.
Edited by Петров Олег Максимович