Project

General

Profile

Actions
Copy link

Feature #7999

closed

Options of the verification tools should not be hardcoded inside Klever

Added by Vadim Mutilin over 7 years ago. Updated over 7 years ago.

Status:
Rejected
Priority:
High
Assignee:
-
Category:
-
Target version:
-
Start date:
02/25/2017
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

Right now there are a number of places where the source code of Klever contains dependencies on the verification tool used, e.g. cpachecker, moreover Klever adds options inside its components (like specification of witness files output path).
All verification tool options should be passed as an input for running Klever. Only BenchExec may know the meaning of options for the tool. For example, an option which specifies a witness file should come together with an option which specifies where to search the witness for BechExec. These two options should be specified as an input for Klever.

In such a way Klever will able:
  1. support any configuration of CPAchecker
  2. support any verification tool supported by BenchExec

Related issues 1 (0 open — 1 closed)

Is duplicate of Klever - Feature #7451: Extract default verifier options from VTG strategies source code to configuration fileClosedIlja Zakharov08/05/2016

Actions
Actions
Copy link

Also available in: Atom PDF