Feature #6807

Separate verification tasks generation and verification results processing

Added by Evgeny Novikov over 4 years ago. Updated almost 3 years ago.

Tasks generation
Target version:
Start date:
Due date:
% Done:


Estimated time:
Published in build:


At the moment Verification Tasks Generator both produces verification tasks on the basis of the abstract ones and a specified configuration and processes verification results including processing of error traces (witnesses), processing of static verifier logs and preparing corresponding reports.

This confuses everybody including me. In particular the same category Tasks generation is used for all relevant issues.

I hope that we can separate them gracefully both in code (in addition we will get one more level of parallelism) and here.

Related issues

Related to Klever - Feature #6608: Generate abstract verification tasks in parallelClosed01/29/2016




Updated by Evgeny Novikov over 4 years ago

Actually we designed this with Ilja as it is now due to Verification Tasks Generator can generate further verification tasks in accordance with processed verification results (e.g. it will be the case with multi-aspect verification - #6692) not only with new abstract verification tasks. So it won't be so easy to separate these functions.


Updated by Evgeny Novikov over 3 years ago

  • Assignee changed from Evgeny Novikov to Ilja Zakharov
  • Priority changed from High to Urgent

Let's do it together with #6608.


Updated by Evgeny Novikov about 3 years ago

  • Target version set to 2.0

Updated by Evgeny Novikov about 3 years ago

  • Target version changed from 2.0 to 0.2

This considerable Core refactoring is always completed and it would be better to have it in master ASAP while Klever 1.0 will be devoted to great conceptual improvements.


Updated by Ilja Zakharov about 3 years ago

  • Status changed from New to Resolved

Implemented in the core-refactoring branch as a part of VTG and AVTG major refactoring.


Updated by Evgeny Novikov almost 3 years ago

  • Status changed from Resolved to Closed

I merged the branch to master in aec48ac1. Please, note that there is a new issue category "Results processing"!

Also available in: Atom PDF