Project

General

Profile

Actions

Feature #11819

open

Try to enable cpa.smg.handleUnknownDereferenceAsSafe=false for CPAchecker SMG

Added by Evgeny Novikov over 1 year ago. Updated over 1 year ago.

Status:
New
Priority:
High
Category:
Tasks generation
Target version:
-
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 #1

Updated by Evgeny Novikov over 1 year ago

  • Target version deleted (3.7)

Let's make this experiment one day later.

Actions

Also available in: Atom PDF