Feature #9459
closed
Feature #8494: Process extended format of violation witnesses
Generate error traces in a new format
Added by Evgeny Novikov almost 6 years ago.
Updated almost 4 years ago.
Category:
Results processing
Description
First of all, see the description of #9458. Also, we plan to eliminate many redundant error trace transformations that sometimes break visualization of found warnings.
- Status changed from New to Resolved
Except for minor issues this is done in branch klever-3.0.
- Status changed from Resolved to Closed
- Status changed from Closed to Resolved
I added support for all our existing extensions to violation witnesses in branch extended-witnesses. They need a new version of CPAchecker while currently corresponding functionality is in the development branch. Bridge update (#9458) is also necessary.
- Related to Feature #9458: Visualize a new format of error traces added
- Status changed from Resolved to Open
Thanks to Pavel we understood that we do not support several notes per one edge though it is useful and it is mentioned in specification of extended violation witnesses.
- Status changed from Open to Resolved
Multiple notes per one violation witness edge (error trace node) were supported in branch extended-witnesses.
- Status changed from Resolved to Closed
Tests passed, so, I merged the branch to master in d74545524.
Also available in: Atom
PDF