Project

General

Profile

Actions
Copy link

Feature #7799

closed

Integrate Ultimate Automizer as an alternative verification tool

Added by Ilja Zakharov about 8 years ago. Updated about 7 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Ilja Zakharov
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 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 open — 2 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
Copy link
 #1

Updated by Ilja Zakharov about 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
Copy link
 #2

Updated by Ilja Zakharov over 7 years ago

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

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
Copy link
 #4

Updated by Evgeny Novikov over 7 years ago

  • Target version set to 2.0
Actions
Copy link
 #5

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

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

Updated by Evgeny Novikov about 7 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
Copy link

Also available in: Atom PDF