Project

General

Profile

Actions
Copy link

Feature #10804

open

Try to disable guessing allocated memory size

Added by Evgeny Novikov over 3 years ago. Updated over 3 years ago.

Status:
New
Priority:
High
Assignee:
Anton Vasilyev
Category:
Preset jobs, marks and tags
Target version:
-
Start date:
04/14/2021
Due date:
% Done:

0%

Estimated time:
Published in build:

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.

Actions
Copy link
 #1

Updated by Evgeny Novikov over 3 years ago

  • 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.

Actions
Copy link
 #2

Updated by Evgeny Novikov over 3 years ago

  • Target version deleted (3.3)

There are more high priority tasks for CPAchecker SMG, so, I do not expect this option soon.

Actions
Copy link

Also available in: Atom PDF