Feature #7452
closed
Allow to overwrite default options specified for verifiers
Added by Evgeny Novikov over 7 years ago.
Updated over 6 years ago.
Category:
Tasks generation
Description
Nowadays users can't overwrite default options specified for verifiers. This feature assumes this just for CPAchecker since the procedure of merging options does strongly depend on how these options are interpreted by a corresponding verifier.
In addition, it is assumed that all conflicts in options should be resolved by failing processing of a corresponding abstract verification task. For instance, if the user wants to use VTG strategy A that needs CPAchecker configuration A1 and additionally will try to use CPAchecker configuration A2 there should be an unknown report rather than any verification task for CPAchecker.
This feature is most important for MPV, since in current master the support of MPV was broken (again). Therefore, it will be done in specification_automata branch, so it could be tests.
It should be done in a separate branch which should be merged to master.
This feature (and related) will be done according with prepared instruction.
This feature was started in branch new_format_of_strategies.
- Assignee deleted (
Vitaly Mordan)
- Priority changed from Urgent to High
This feature should be implemented, first, after blocking #7451, second, in a branch from master. Any way we can live without it right now. Soon I will implement a couple of workarounds specially for some seldom use cases to deal with it.
This feature was implemented in branch new_format_of_strategies.
It is possible to use preset configurations (for example, 'bit precision analysis') or specify config by its name. If no configuration was specified, '-ldv' will be used for instrumentation.
- Assignee set to Ilja Zakharov
- Priority changed from High to Urgent
Let's do it together with #6608.
- Target version set to 2.0
- 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.
- Status changed from New to Resolved
Implemented in the core-refactoring branch as a part of VTG and AVTG major refactoring.
- Status changed from Resolved to Closed
I merged the branch to master in aec48ac1.
Also available in: Atom
PDF