Actions
Feature #11819
openTry to enable cpa.smg.handleUnknownDereferenceAsSafe=false for CPAchecker SMG
Start date:
08/10/2022
Due date:
% Done:
0%
Estimated time:
Published in build:
Description
Currently CPAchecker does not immediately fail when it encounters dereferences of unknown pointers. In some cases it can result in weird false alarms later and much efforts may be necessary to find root causes. In case of that option CPAchecker should report unsafes earlier and they should be clearer. Unfortunately, there may be too many unsafes demonstrating a lot of blanks in the environment (model).
Actions