Feature #11624
closed
Develop model for struct_size()
Added by Evgeny Novikov almost 2 years ago.
Updated almost 2 years ago.
Category:
Environment models
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.
- 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.
- 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.
Also available in: Atom
PDF