Project

General

Profile

Actions

Feature #7799

closed

Integrate Ultimate Automizer as an alternative verification tool

Added by Ilja Zakharov over 7 years ago. Updated over 6 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Category:
Tasks generation
Target version:
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 open3 closed)

Feature #7800: Refactoring of VTGClosedIlja Zakharov12/13/2016

Actions
Feature #7801: Increase size of the report component name to 20 from 15ClosedVladimir Gratinskiy12/13/2016

Actions
Feature #7803: Shrink verifier name to 20 symbolsRejected12/14/2016

Actions

Related issues 3 (1 open2 closed)

Has duplicate Klever - Feature #6747: Support UAtomizer as one of Klever verification back-endsRejected02/03/2016

Actions
Blocks Klever - Feature #6552: Implement Cluster SchedulerNewIlja Zakharov01/28/2016

Actions
Blocked by Klever - Feature #7452: Allow to overwrite default options specified for verifiersClosedIlja Zakharov08/05/2016

Actions
Actions #1

Updated by Ilja Zakharov over 7 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 #2

Updated by Ilja Zakharov almost 7 years ago

  • Category set to Tasks generation
  • Assignee set to Ilja Zakharov
Actions #3

Updated by Evgeny Novikov almost 7 years ago

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

Actions #4

Updated by Evgeny Novikov over 6 years ago

  • Target version set to 2.0
Actions #5

Updated by Evgeny Novikov over 6 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 #6

Updated by Ilja Zakharov over 6 years ago

  • Status changed from Open to Resolved

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

There can be problems with witnesses still because all our tools do this differently, unfortunately.

Actions #7

Updated by Evgeny Novikov over 6 years ago

  • Status changed from Resolved to Closed

I merged the branch to master in aec48ac1. At last we have two really different static verification tools in master!

Actions

Also available in: Atom PDF