Bug #10930
closed
Fix memory allocation via $ALLOC in EMG specifications
Added by Ilja Zakharov over 2 years ago.
Updated over 2 years ago.
Category:
Environment models
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.
- Status changed from New to Resolved
The fix is in the fix-alloc branch.
- Status changed from Resolved to Open
Tests did not pass, we need to investigate reasons of changes.
- Blocked by Feature #10486: Develop environment model specification for inode_operations added
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.
- Related to Feature #10944: Allocate external data for platform_device.dev.platform_data added
- Related to deleted (Feature #10944: Allocate external data for platform_device.dev.platform_data)
- Blocked by Feature #10944: Allocate external data for platform_device.dev.platform_data added
- 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.
- 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.
Also available in: Atom
PDF