Project

General

Profile

Feature #7452

Allow to overwrite default options specified for verifiers

Added by Evgeny Novikov about 4 years ago. Updated about 3 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

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.


Related issues

Blocked by Klever - Feature #7451: Extract default verifier options from VTG strategies source code to configuration fileClosed08/05/2016

Actions
Blocks Klever - Feature #7453: Clarify conception of resource limits for one abstract verification taskRejected08/05/2016

Actions
Blocks Klever - Feature #7448: Add property automata for all rulesRejected06/27/201606/27/2016

Actions
Blocks Klever - Feature #7799: Integrate Ultimate Automizer as an alternative verification toolClosed12/13/2016

Actions

History

#1

Updated by Vitaly Mordan about 4 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.

#2

Updated by Evgeny Novikov about 4 years ago

It should be done in a separate branch which should be merged to master.

#3

Updated by Vitaly Mordan about 4 years ago

This feature (and related) will be done according with prepared instruction.

#4

Updated by Vitaly Mordan about 4 years ago

This feature was started in branch new_format_of_strategies.

#5

Updated by Evgeny Novikov about 4 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.

#6

Updated by Vitaly Mordan about 4 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.

#7

Updated by Evgeny Novikov over 3 years ago

  • Assignee set to Ilja Zakharov
  • Priority changed from High to Urgent

Let's do it together with #6608.

#8

Updated by Evgeny Novikov about 3 years ago

  • Target version set to 2.0
#9

Updated by Evgeny Novikov about 3 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.

#10

Updated by Ilja Zakharov about 3 years ago

  • Status changed from New to Resolved

Implemented in the core-refactoring branch as a part of VTG and AVTG major refactoring.

#11

Updated by Evgeny Novikov about 3 years ago

  • Status changed from Resolved to Closed

I merged the branch to master in aec48ac1.

Also available in: Atom PDF