Feature #11624
closedDevelop model for struct_size()
0%
Description
Quite many drivers use struct_size() to compute sizes of memory areas to be occupied by structures with zero length arrays. Underlying function __ab_c_size() uses __builtin_mul_overflow() that is not known to the verifier. Corresponding models are necessary.
Updated by Evgeny Novikov over 2 years ago
- Status changed from New to Resolved
I developed models in branch overflow-models. Moreover, I fixed models for memory allocating functions, so that now they return NULL when one tries to allocate memory areas of the SIZE_MAX size. Corresponding test cases were added. Now CI runs tests.
Updated by Evgeny Novikov over 2 years ago
- Status changed from Resolved to Closed
After some minor fixes tests passed. So I merged the branch to master in 8ec92b492. Verification of ~2000 drivers of Linux 5.5 against memory safety and drivers:clk2 demonstrated several improvements. Now it may be easier to understand that some functions need models.