Feature #7451

Extract default verifier options from VTG strategies source code to configuration file

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

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


Estimated time:
Published in build:


From very ancient times verifier options were specified in jobs, in VTG strategies and in schedulers. I fixed this for schedulers, but just move options to VTG strategies. So now VTG strategies are the only Klever components for which default options are specified in jobs in source code (what is about LKVOG?..). I suppose to place near "linux-3.14/rule specs.json" (the rule specifications base) "verifier.json" where all default options for various strategies and verifiers should be specified. This file will be symlinked by other existing preset jobs.

Recently several new rule specifications, namely, generic:memory and sync:race, we introduced and required dedicated verifier versions, configurations and options. That's why in addition I suppose to specify all these things both globally and for corresponding properties. From this point of view it has sense to specify them not in a separate configuration file but directly within rule specs.json.

Related issues

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

Has duplicate Klever - Feature #7999: Options of the verification tools should not be hardcoded inside KleverRejected02/25/2017

Blocks Klever - Feature #7452: Allow to overwrite default options specified for verifiersClosed08/05/2016

Blocks Klever - Feature #8175: Add support for high-level interface to static verifiersNew04/26/2017




Updated by Evgeny Novikov about 4 years ago

  • Assignee deleted (Vitaly Mordan)
  • Priority changed from Urgent to High

It is quite tedious work that should be done later since the major use cases work although not very nice.


Updated by Evgeny Novikov over 3 years ago

  • Assignee set to Ilja Zakharov
  • Priority changed from High to Urgent

Let's do it together with #6608.


Updated by Evgeny Novikov over 3 years ago

  • Description updated (diff)

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.

From now everybody can easily configure existing and new static verification tools on the fly.

Also available in: Atom PDF