Project

General

Profile

Actions

Feature #9305

open

Provide a list of undefined and modelled functions for a fragment under verification

Added by Ilja Zakharov over 5 years ago. Updated about 5 years ago.

Status:
New
Priority:
High
Assignee:
Category:
Environment models
Target version:
-
Start date:
10/04/2018
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

As we claim that our static verification is sound we need to provide some information about preconditions of verification. As a first step in this direction we propose to collect which functions are undefined and for which of them models exist. This should help to understand how many specifications to model functions a user should prepare.

Actions #1

Updated by Vadim Mutilin over 5 years ago

The user would like to know how many specifications of the active part of an environment she need to prepare. Is it part of this task?

Actions #2

Updated by Ilja Zakharov over 5 years ago

If you mean entry points then it is not a part of this task. Entry points can be easily found from the coverage report. This issue is related to external functions that can be completely undefined or be modelled. Currently, we do not have any report concerning this part of a program fragment under verification.

Actions #3

Updated by Vadim Mutilin over 5 years ago

Yes, I'm talking about entry_points and I do not see how they can be found from the coverage report "easily"

Actions #4

Updated by Evgeny Novikov over 5 years ago

Let's open another issue that will aim at showing some information on unspecified project specific API. For instance, for Linux loadable kernel modules this API includes uncovered exported functions and all global variables having structure types and which fields are initialized with function pointers.

Actions #5

Updated by Evgeny Novikov about 5 years ago

  • Priority changed from Urgent to High
  • Target version deleted (3.0)

There is not a particular plan in this direction.

Actions

Also available in: Atom PDF