Project

General

Profile

Actions

Feature #7435

closed

Support of several verifiers is required

Added by Vitaly Mordan over 8 years ago. Updated over 4 years ago.

Status:
Rejected
Priority:
Normal
Assignee:
-
Category:
-
Target version:
-
Start date:
07/29/2016
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

Currently Klever supports only 1 hard-coded verifier:
"cpachecker location": "..."
and it is impossible to use several verifiers (or different versions of one).
For example, tests for rule specifications should be passed on all supported verifiers and for all existed models (such as property automata and instrumentation), therefore, in general case test job file should be working with different verifiers.
It is suggested to support the following format in configuration:
"verifiers": [
[ {"Alias": "..."}, {"location": "..."}
],
...
[ {"Alias": "..."}, {"location": "..."}
]]
Then it would be possible to use the required verifier in job file by its alias:
"verifier": {
"name": <verifier alias>,
...


Related issues 3 (0 open3 closed)

Related to Klever - Bug #7394: Restore support for property automata rule specificationsClosedVitaly Mordan06/24/201606/24/2016

Actions
Related to Klever - Feature #6699: Native scheduler does not take care of verifier versionClosedIlja Zakharov02/02/2016

Actions
Blocks Klever - Feature #7467: Establish Sequential Combination of MAV and MPV methodsRejectedVitaly Mordan06/28/201606/28/2016

Actions
Actions

Also available in: Atom PDF