Actions
Feature #7435
closedSupport of several verifiers is required
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>,
...
Actions