Feature #7481
open
Try to use memory allocating function models by default
Added by Evgeny Novikov over 8 years ago.
Updated about 7 years ago.
Category:
Requirement specifications
Description
After EMG and CPAchecker became very accurate regarding tracking memory (#7465 and #7454) we need to model as much memory allocating functions as possible. Good news is that the most of them already have models since we have the rule specification for checking common memory leaks. Unfortunately some such functions haven't models. For instance, spi_alloc_master() is such the function. Due to this we lose one target bug (c822fb57ba12~/drivers/spi/spi-pxa2xx-platform.ko/linux:clk1).
Do we have a ticket to generate models for allocation functions automatically as kernel core models?
- Priority changed from Urgent to High
In c5ded90 I at last added model for spi_alloc_master(). After that both both before and after the target bug fix I got timeouts.
Let's discover and experiment with this issue one day later.
- Priority changed from High to Urgent
I will continue this work since it is very required for several properties to be verified without many false alarms.
We need to also add model for devm_kzalloc() since its absence causes false alarms for different rules.
Evgeny Novikov wrote:
We need to also add model for devm_kzalloc() since its absence causes false alarms for different rules.
Actually Anton already did that for generic:memory, so it seems that we just need to get his models and use them for all rules by default.
- Priority changed from Urgent to High
Let's fix and improve specifications after we will have good tests and a testing infrastructure (version:0.3) and likely after we will complete a considerable refactoring of Core (1.0).
Also available in: Atom
PDF