Klever

Eventually branch check-callback-resources contains the framework for checking callback resources. Indeed, it does more than only testing whether the same resources are passed to various related callbacks. By storing, checking and releasing resources it also verifies a correctness of an order of invoked callbacks.

In some cases it stumbles across some complicated issues with environment model specifications. For instance, it may be necessary to relate platform devices with devices passed to power management callbacks. Otherwise, Klever finds unexpected unsafes. Unfortunately, I could not do that (either environment model specifications or EMG does not support this or I did something wrong). Besides, this one as well as some other issues are actually open questions to the kernel behavior. This does not belong directly to the given issue, but it prevents its completion. You can see several blocking, already resolved issues. Several more issues should be added and fixed prior to this one can be closed.

Another point is that there are numerous timeouts for rather simple test cases after adding this framework and appropriate checks. It may be an issue in CPAchecker BAM since CPAchecker SMG can handle corresponding verification tasks very fast. Also, this can point out some extra problems with environment model specifications.

All in all, the framework and checks are useful, but more work is necessary to accept them and enable them within CI.