Klever

I implemented models and tests for the list API in branch list-models-and-tests. Most related false alarms, that were obtained at verification of Linux 5.19-rc7 against memory safety, became either safes or unknowns. In some cases there are still unsafes, but they are either quite complicated (it is not clear whether list operations are responsible for them) or they have other error traces than before. Let's carefully test these models as they quite vital.

CI revealed numerous degradations due to old versions of the Linux kernel do not have the header included by the new model. Moreover, there are some transitions to be carefully studied.

I fixed inclusion of headers so that everything seems to work well for all considered versions of the Linux kernel. Moreover, I scrutinized transitions. They correspond to positive regressions thanks to models of the list API. Let's see on CI results one more time and, more important, let's evaluate how these models affect verification of a bunch of drivers against various requirement specifications.

I was very wondered, that adding models for the list API resulted in several positive, expected regressions, but nothing changed considerably. It is the case both for checking memory safety and drivers:clk2 requirements specification. So I merged the branch to master in 40c9ccc3e.