Feature #7452
closedAllow to overwrite default options specified for verifiers
0%
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.
Updated by Vitaly Mordan over 8 years ago
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.
Updated by Evgeny Novikov over 8 years ago
It should be done in a separate branch which should be merged to master.
Updated by Vitaly Mordan over 8 years ago
This feature (and related) will be done according with prepared instruction.
Updated by Vitaly Mordan over 8 years ago
This feature was started in branch new_format_of_strategies.
Updated by Evgeny Novikov over 8 years ago
- 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.
Updated by Vitaly Mordan over 8 years ago
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.
Updated by Evgeny Novikov over 7 years ago
- Assignee set to Ilja Zakharov
- Priority changed from High to Urgent
Let's do it together with #6608.
Updated by Evgeny Novikov about 7 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 7 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 about 7 years ago
- Status changed from Resolved to Closed
I merged the branch to master in aec48ac1.