Project

General

Profile

Actions

Feature #7451

closed

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

Added by Evgeny Novikov over 7 years ago. Updated over 6 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Category:
Tasks generation
Target version:
Start date:
08/05/2016
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

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 4 (1 open3 closed)

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

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

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

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

Actions
Actions

Also available in: Atom PDF