Project

General

Profile

Actions
Copy link

Feature #11624

closed

Develop model for struct_size()

Added by Evgeny Novikov over 2 years ago. Updated over 2 years ago.

Status:
Closed
Priority:
High
Assignee:
Evgeny Novikov
Category:
Environment models
Target version:
3.6
Start date:
05/30/2022
Due date:
% Done:

0%

Estimated time:
Published in build:

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.

Actions
Copy link
 #1

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.

Actions
Copy link
 #2

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.

Actions
Copy link

Also available in: Atom PDF