Project

General

Profile

Actions

Feature #7237

closed

Improve existing rule specifications

Added by Evgeny Novikov over 8 years ago. Updated over 8 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Category:
-
Target version:
-
Start date:
06/24/2016
Due date:
06/24/2016
% Done:

0%

Estimated time:
Published in build:

Description

This feature includes numerous improvements (some of them can be treated even as bug fixes) in existing rule specifications that should be accomplished with developing quite thorough test cases and a bugs/rules database.

For the latter I suggest to use a single JSON file containing the tree of bugs/rules with identifiers, short descriptions and links to bug reports. IMHO it is enough, providing detailed descriptions of API as well as source code with/without bugs is hard to develop and maintain. The former can be found in an appropriate documentation, while the latter is likely can be found by following provided links with many useful details and discussions.

When this feature will be implemented, we will initiate considerable redesign of everything related with the following:
  • how users will choose what rules to verify and how to verify them,
  • how to keep and to visualize verification results (I don't think that there will be many changes, just attribute rule specification will disappear while attribute bug(rule) will become mandatory),
  • corresponding support in the back end (Klever Core) - too much to describe it here.

The related work was already started in branch rule_specs_tests.


Related issues 3 (0 open3 closed)

Related to Klever - Feature #6912: Support for several advices for memory allocation functions (kzalloc)ClosedVitaly Mordan03/01/2016

Actions
Blocks Klever - Feature #6779: Adapt rule specifications from LDV ToolsClosedVitaly Mordan02/03/2016

Actions
Follows Klever - Bug #7333: Fix nonstandard verification tasks generation strategiesClosedVitaly Mordan06/23/2016

Actions
Actions #1

Updated by Vitaly Mordan over 8 years ago

Currently this work was placed in the branch private/merge_test, in which:
- New format of rule specification description was used based on mav branch and the latest master (irq/post probe/etc.);
- rule specifications was decomposed when needed based on linux kernel API;
- each rule specification is equipped with the set of tests.
It is suggested to unify all rule specifications (such as http://forge.ispras.ru/issues/6912 and http://forge.ispras.ru/issues/6779) to this format and merge them into this branch.

Actions #2

Updated by Evgeny Novikov over 8 years ago

Why did you merge the mav branch into this one?! This issue was intended just for refactoring existing rule specifications while the mav branch introduces very many things that are still based on the very poor theory and thus dreadful by design. The branch mav should be deleted at all when we will carefully design and implement the new way to specify requirements to be checked and the new way to check them. Just some parts of code from that branch can be taken into the new one. Please, remove it from the branch of this feature so that I will be able to merge into master.

And I didn't see the requirements database that is needed much more than MAV features.

Please, do not even think to do something more with this until the theory will be strong enough. You have already spent very much time for doing experimental things that will not find their way to master ever.

Actions #3

Updated by Vitaly Mordan over 8 years ago

The main idea of this branch is to unify all formats of rule specification description (now there are at least 3 different formats with some rule specifications).
Branch mav has some base improvements (such as support of bug kinds, parameters for models, common aspects, etc.), which are needed for master, as well as the latest master get some useful features (support for testing, new EMG, etc.).
It is suggested to prepare all our rule specifications with tests in this branch, evaluate them on all modules and after that merge into master. By that time most likely improved branch mav also will be merged, so there will be no conflicts.

Actions #4

Updated by Evgeny Novikov over 8 years ago

Vitaly Mordan wrote:

The main idea of this branch is to unify all formats of rule specification description (now there are at least 3 different formats with some rule specifications).

Why did you decide so? One more time, this issue is intended just for refactoring existing rule specifications. Just some small improvements for a future still unrevealed approach were assumed, e.g. specify "bug kinds" in comments near corresponding asserts.

Branch mav has some base improvements (such as support of bug kinds, parameters for models, common aspects, etc.), which are needed for master, as well as the latest master get some useful features (support for testing, new EMG, etc.).

Improvements from branch mav in their current state aren't required in master at all.

It is suggested to prepare all our rule specifications with tests in this branch, evaluate them on all modules and after that merge into master. By that time most likely improved branch mav also will be merged, so there will be no conflicts.

Branch mav should be deleted while absolutely new approach mentioned in description of this feature request will be implemented. Just some experience and source code from that branch can be taken.

Actions #5

Updated by Evgeny Novikov over 8 years ago

  • Status changed from New to Closed

I merged into master in 3d883ae (v0.1rc5) the branch that in addition brings very-very much functionality that wasn't required neither for improving existing rule specifications nor at all.

BTW, this merge was the most awful one in all my life. We should avoid such situations in future.

Actions

Also available in: Atom PDF