Project

General

Profile

Actions
Copy link

Bug #10930

closed

Fix memory allocation via $ALLOC in EMG specifications

Added by Ilja Zakharov about 3 years ago. Updated about 3 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Ilja Zakharov
Category:
Environment models
Target version:
3.3
Start date:
09/09/2021
Due date:
% Done:

0%

Estimated time:
Detected in build:
git
Platform:
Published in build:

Description

There are two specific expressions to allocate memory:
  • $ALLOC - allocate memory with sizeof.
  • $UALLOC - allocate memory with undefined size.

Currently they both result in allocating memory with an unknown size. This should be fixed.

Related issues 2 (0 open — 2 closed)

Blocked by Klever - Feature #10486: Develop environment model specification for inode_operationsClosedIlja Zakharov08/31/2020

Actions
Blocked by Klever - Feature #10944: Allocate external data for platform_device.dev.platform_dataClosedEvgeny Novikov09/16/2021

Actions
Actions
Copy link
 #1

Updated by Ilja Zakharov about 3 years ago

  • Status changed from New to Resolved

The fix is in the fix-alloc branch.

Actions
Copy link
 #2

Updated by Evgeny Novikov about 3 years ago

  • Status changed from Resolved to Open

Tests did not pass, we need to investigate reasons of changes.

Actions
Copy link
 #3

Updated by Evgeny Novikov about 3 years ago

  • Blocked by Feature #10486: Develop environment model specification for inode_operations added
Actions
Copy link
 #4

Updated by Evgeny Novikov about 3 years ago

At least we need to finish the environment model for inodes, dentries and so on to avoid numerous false alarms due to the old (yet current) model for debugfs_create_file() allocate memory that can leak due to drivers can ignore return values of the appropriate function.

Actions
Copy link
 #5

Updated by Evgeny Novikov about 3 years ago

  • Related to Feature #10944: Allocate external data for platform_device.dev.platform_data added
Actions
Copy link
 #6

Updated by Evgeny Novikov about 3 years ago

  • Related to deleted (Feature #10944: Allocate external data for platform_device.dev.platform_data)
Actions
Copy link
 #7

Updated by Evgeny Novikov about 3 years ago

  • Blocked by Feature #10944: Allocate external data for platform_device.dev.platform_data added
Actions
Copy link
 #8

Updated by Evgeny Novikov about 3 years ago

  • Status changed from Open to Resolved

I fixed one more issue with allocating memory by the debugfs_create_file() model in the same branch. Let's see on testing results.

Actions
Copy link
 #9

Updated by Evgeny Novikov about 3 years ago

  • Status changed from Resolved to Closed

In addition to CI tests that demonstrated improvements in verification results, I considered changes at verification of ~2000 drivers against memory safety and drivers:clk.*. The former demonstrated that verification tasks became more complex that is an expected change due to the verification tool has to track and check more things with accurate memory allocation. Besides, in some cases the verification tool started to report Unsafes instead of wrong result. The latter demonstrated several strange transitions from Unsafe to Safe but it is unlikely that somebody will investigate this. There were several changes from/to different failures in CPAchecker for both requirement specifications.

Ultimately, I consider that this bug fix is crucial and strictly necessary. Let's make environment models more and more accurate. I merged the branch to master in 620be6b12.

Actions
Copy link

Also available in: Atom PDF