Project

General

Profile

Actions
Copy link

Feature #11819

open

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

Added by Evgeny Novikov over 2 years ago. Updated about 2 years ago.

Status:
New
Priority:
High
Assignee:
Evgeny Novikov
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
Copy link
 #1

Updated by Evgeny Novikov about 2 years ago

  • Target version deleted (3.7)

Let's make this experiment one day later.

Actions
Copy link

Also available in: Atom PDF