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)
- *
-smgterminates 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 Васильев Антон Александрович