Feature #11459
closed
Improve support for Linux 5.17
Added by Evgeny Novikov about 2 years ago.
Updated about 2 years ago.
Category:
Environment models
Description
This is almost like #11458, but it is dedicated to Linux 5.17 that will be released pretty soon.
The last obvious thing to do for this feature request is to develop models for mem*() functions that have some definitions in new versions of the Linux kernel (for instance, you can see at include/linux/fortify-string.h of Linux 5.17). These definitions introduce some redundant checks and confuse CPAchecker SMG that expect pure mem*() function calls rather than, say, __builtin_mem*() function calls. Indeed, this issue is not new, e.g. memset() has it even in Linux 3.14 but only for the ARM architecture (you can see at arch/arm/include/asm/string.h).
Let's wait while Anton will support a better way to provide a list of appropriate functions.
- Status changed from New to Resolved
After Anton has added support to specify custom mem*() functions for CPAchecker SMG, I added necessary models and corresponding tests passed. This finishes considerable improvement of specifications and all the necessary things to support Linux 5.17 better. Let's wait for CI results.
- Status changed from Resolved to Closed
After numerous fixes CI passed tests. Moreover, I evaluated changes for ~2000 drivers of the Linux kernel. Verification results for Linux 5.5 and Linux 5.17 demonstrated even more importance of development of new function models (quite many false alarms were revealed after fixed models for mem*() functions). Besides, some warnings look strange and this is likely a deal for fixing CPAchecker SMG. Anyway, all these issues are not related to the given one and, thus, they should be considered separately.
I merged the branch to master in 1633a0f37. Enjoy!
Also available in: Atom
PDF