Project

General

Profile

Actions

Feature #9271

open

Main generation with information about sharedness of parameters

Added by Pavel Andrianov about 6 years ago. Updated almost 6 years ago.

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

0%

Estimated time:
Published in build:

Description

Mostly for special operating systems the main is based on a list of functions, which should be called. The parameters of the function call should not be just alloced, as they should be shared most of the times. However, some of the arguments are known to be local, for example, user provided string. And this memory can not be participate in data race. So, there is a need to specify such cases. This issue requires the improvement of simple main specification: it is not only a list of functions, but also contains a description of some arguments.


Related issues 1 (1 open0 closed)

Related to Klever - Feature #9272: Main generation without info-requestsNewIlja Zakharov09/11/2018

Actions
Actions #1

Updated by Evgeny Novikov about 6 years ago

  • Priority changed from Normal to Urgent
  • Target version set to 2.0

This is required to verify some C software. Klever 2.0 will provide a very flexible environment model generator, so, it should not be a complex task for it.

Actions #2

Updated by Evgeny Novikov about 6 years ago

  • Related to Feature #9272: Main generation without info-requests added
Actions #3

Updated by Evgeny Novikov about 6 years ago

  • Target version changed from 2.0 to 3.0

Let's postpone these not so important issues as Klever 2.0 is too large already.

Actions #4

Updated by Evgeny Novikov almost 6 years ago

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

I am not sure that we will be able to this in Klever 3.0.

Actions

Also available in: Atom PDF