Klever

I did this in branch notes-level-2. Also, I had to get rid of a very old workaround that was used because of "ASSERT" comments were used on normal paths.

CI demonstrated a tremendous number of regressions to be fixed.

After fixes CI passed tests. Unfortunately, invocation of __VERIFIER_assume() through the intermediate function adding a note resulted in too considerable changes in verification results (Pavel investigated that this is likely due to the solver considers the corresponding formulas rather differently). That's why I had to revert this change and to add the note in a cheating way.

Tests passed, so, I merged the branch to master in fd6a483c8. Please, note, that all out-of-tree requirement specifications using ldv_assert() should be adjusted so that they should not pass any value/expression to this function while they should invoke it just when the corresponding value/expression is not true. Besides, there should be comment ASSERT like in the following example:

    if (ldv_iomem != 0)
        /* ASSERT io-memory should be released at exit */
        ldv_assert();