Klever

Done in 'emg-alloc' branch.

For all user specified interfaces corresponding memory allocations now are correct allocations with proper sizeof if corresponding EMG option "allocate with sizeof" is set (made it True by default because it applies only for user specified interfaces since now).

By the way target bug cannot be found because function 'spi_alloc_master' has no model and not tracked as a memory allocating function. But, for example, for false positive in drivers/usb/misc/cytherm.ko (rule linux:usb:dev) new allocation helps to prove driver correctness (new verdict is safe).

I merged the given branch to master in 0c2b0af. Since EMG becomes more and more accurate we definitely need CPAchecker that can deal with that (#7454).

First look at results showed that sometimes (often) it isn't enough to allocate just memory for callback parameters. For instance, for USB devices pointers to USB interfaces that are just fields of structure usb_device are passed to callbacks. But callbacks quickly get USB devices by using container_of. For the latter memory isn't allocated at all that leads to false alarms as before.

Moreover it seems that environment models don't need to allocate any memory in this case at all! One can try to simply pass to callbacks pointers to corresponding variables of type structure usb_device keeping these callbacks.

The only thing environment models should do in ideal - is to distribute USB interfaces between various modules (devices) but likely we don't need this right now.

I suggest to investigate other false alarms on rule specification linux:usb:dev.

Evgeny, please, close the bug and open the separate one for a particular false alarm. The requested feature is implemented and works as it should do and you are speaking abut a significantly different feature request which is more relevant to specifications improvement.

One more step to the specified target was done in branch emg-usb-device that was merged to master in abe8578. In future let's create more concrete issues when some problems with particular interfaces will be thoroughly investigated.