Feature #10804
open
Try to disable guessing allocated memory size
Added by Evgeny Novikov over 3 years ago.
Updated over 3 years ago.
Category:
Preset jobs, marks and tags
Description
At the moment CPAchecker SMG allocates 2 bytes of memory when it cannot evaluate a memory size to be allocated. Most likely, this will result in memory issues later like for driver drivers/platform/chrome/cros-ec-sensorhub.ko of Linux 5.12-rc3, x86_64, allmodconfig. I suggest to fail immediately rather than to do this later and provide more obscure error reports. Of course, we will need to evaluate the change thoroughly.
- Target version changed from 3.2 to 3.3
Anton pointed out option "cpa.smg.guessSizeOfUnknownMemorySize=false" that results to an exception UnsupportedCodeException for the given case rather than guessing that 2 bytes are allocated. This way does not help users to identify places required some adjustments, say, setting some structure field in the environment model. Also, he has plans to support one more option to output violation witnesses that will accurately refer to those places where allocated memory sizes can not be calculated. Let's try to use that option when it will be ready.
- Target version deleted (
3.3)
There are more high priority tasks for CPAchecker SMG, so, I do not expect this option soon.
Also available in: Atom
PDF