Feature #11459
closedImprove support for Linux 5.17
0%
Description
This is almost like #11458, but it is dedicated to Linux 5.17 that will be released pretty soon.
Updated by Evgeny Novikov about 2 years ago
- Blocked by Feature #11458: Improve support for Linux 5.10 added
Updated by Evgeny Novikov about 2 years ago
- Related to Feature #11465: Update CIF added
Updated by Evgeny Novikov about 2 years ago
- Blocked by Feature #11444: Update CPAchecker SMG added
Updated by Evgeny Novikov about 2 years ago
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.
Updated by Evgeny Novikov about 2 years ago
- 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.
Updated by Evgeny Novikov almost 2 years ago
- Blocked by deleted (Feature #11444: Update CPAchecker SMG)
Updated by Evgeny Novikov almost 2 years ago
- 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!