Klever

Category:

Tasks generation

Target version:

0.2

Start date:

12/13/2016

Due date:

% Done:

100%

Estimated time:

(Total: 0.00 h)

Published in build:

Description

Ultimate Automizer is a one of the best verification tools concerning its results at sv-comp 2016 on Linux device drivers category. Be the way there are several subtasks should be done to run the tool within Klever system.

Subtasks 3 (0 open — 3 closed)

Feature #7800: Refactoring of VTG

Closed

12/13/2016

Feature #7801: Increase size of the report component name to 20 from 15

Closed

Vladimir Gratinskiy

12/13/2016

Feature #7803: Shrink verifier name to 20 symbols

Rejected

12/14/2016

Related issues 3 (1 open — 2 closed)

Has duplicate Klever - Feature #6747: Support UAtomizer as one of Klever verification back-ends

Rejected

02/03/2016

Blocks Klever - Feature #6552: Implement Cluster Scheduler

New

01/28/2016

Blocked by Klever - Feature #7452: Allow to overwrite default options specified for verifiers

Closed

08/05/2016

Issue # Delay: days Cancel

History
Notes
Property changes

Actions

Updated by Ilja Zakharov almost 8 years ago

Status changed from New to Open

Current development is placed in ultimate-backend branch.

Ultimate automizer can work now with klever but there are some issues that should be solved within the tool to complete integration:

Make it possible to run the tool from a directory outside of the tool directory. Currently it is necessary to make many symlinks to do that.
Provide options to place a witness report to a particular dir. Currently scheduler should copy it manually instead of Benchexec (For CPAchecker Benchexec does it automatically).
Prevent creation of temporary files in a user home dir. I have done it by fixing a wrapper script manually.
Add FunctionEntry and Exit attributes to error witnesses edges. Without it trace is very ugly.
Use string references in a witness report to files from line directives instead of cilled file.
Use a proper namespace in witness XML to prevent parser modification. Namespaces for CPAchecker and Ultimate witnesses are a bit different.

Actions

Updated by Ilja Zakharov over 7 years ago

Category set to Tasks generation
Assignee set to Ilja Zakharov

Actions

Updated by Evgeny Novikov over 7 years ago

Let's do it together with #7452 to confirm that new verification backends can be quite easily integrated and configured.

Actions

Updated by Evgeny Novikov about 7 years ago

Target version set to 2.0

Actions

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.

Actions