Feature #7481
openTry to use memory allocating function models by default
0%
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).
Updated by Alexey Khoroshilov over 7 years ago
Do we have a ticket to generate models for allocation functions automatically as kernel core models?
Updated by Evgeny Novikov over 7 years ago
- 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.
Updated by Evgeny Novikov over 7 years ago
- 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.
Updated by Evgeny Novikov about 7 years ago
We need to also add model for devm_kzalloc() since its absence causes false alarms for different rules.
Updated by Evgeny Novikov about 7 years ago
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.
Updated by Evgeny Novikov over 6 years ago
- 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).