Project

General

Profile

Actions

Bug #10930

closed

Fix memory allocation via $ALLOC in EMG specifications

Added by Ilja Zakharov 10 months ago. Updated 10 months ago.

Status:
Closed
Priority:
Urgent
Assignee:
Category:
Environment models
Target version:
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 open2 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 #1

Updated by Ilja Zakharov 10 months ago

  • Status changed from New to Resolved

The fix is in the fix-alloc branch.

Actions #2

Updated by Evgeny Novikov 10 months ago

  • Status changed from Resolved to Open

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

Actions #3

Updated by Evgeny Novikov 10 months ago

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

Updated by Evgeny Novikov 10 months 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 #5

Updated by Evgeny Novikov 10 months ago

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

Updated by Evgeny Novikov 10 months ago

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

Updated by Evgeny Novikov 10 months ago

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

Updated by Evgeny Novikov 10 months 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 #9

Updated by Evgeny Novikov 10 months 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

Also available in: Atom PDF