Project

General

Profile

Feature #9931

Introduce specific comments and error trace actions to distinguish important environment models

Added by Evgeny Novikov 7 months ago. Updated 5 months ago.

Status:
Closed
Priority:
Urgent
Assignee:
Category:
Environment model
Target version:
Start date:
11/18/2019
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

Some environment models can result in faults. Typical examples are the following:

  1. Assertions can fail within ldv_check_final_state().
  2. CPAchecker SMG can reveal, say, memory leaks, when an environment model frees memory for object for which another environment model allocated memory and that was passed to a driver callback that allocated but did not free another memory.

In both cases corresponding actions are not callback actions by definition (although the first one is called so by mistake), so, they are not included in error trace patterns of unsafe marks. This is wrong, since these patterns miss error trace parts important from the point of view of checking.

History

#1

Updated by Evgeny Novikov 7 months ago

  • Description updated (diff)
#2

Updated by Ilja Zakharov 6 months ago

The second part of the task has nothing to do with actions. And there are many reasons why I cannot remove numerical suffixes from names. There are two main reasons:
  • Identifiers helps to distinguish wrappers around static functions with the same names. The only unique attribute that I can use in the case is a file name but it is too long to use it in function names.
  • EMG adds identifiers to distinguish so called instances that can define or call similar artificial functions. Instances do not have names, so I use identifiers.
#3

Updated by Evgeny Novikov 6 months ago

  • Description updated (diff)

Ilja Zakharov wrote:

The second part of the task has nothing to do with actions. And there are many reasons why I cannot remove numerical suffixes from names. There are two main reasons:
  • Identifiers helps to distinguish wrappers around static functions with the same names. The only unique attribute that I can use in the case is a file name but it is too long to use it in function names.
  • EMG adds identifiers to distinguish so called instances that can define or call similar artificial functions. Instances do not have names, so I use identifiers.

Let's try to avoid numbers when it is possible. I moved this task to #9988.

#4

Updated by Evgeny Novikov 6 months ago

  • Category set to Environment model
#5

Updated by Ilja Zakharov 6 months ago

Implemented in error-traces.

#6

Updated by Ilja Zakharov 6 months ago

  • Status changed from New to Resolved
#7

Updated by Evgeny Novikov 5 months ago

  • Status changed from Resolved to Closed

In master.

Also available in: Atom PDF