Integrate Ultimate Automizer as an alternative verification tool
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.
Updated by Ilja Zakharov almost 4 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.