Feature #9459
closedFeature #8494: Process extended format of violation witnesses
Generate error traces in a new format
0%
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.
Updated by Evgeny Novikov over 4 years ago
- Status changed from New to Resolved
Except for minor issues this is done in branch klever-3.0.
Updated by Evgeny Novikov over 3 years ago
- 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.
Updated by Evgeny Novikov over 3 years ago
- Related to Feature #9458: Visualize a new format of error traces added
Updated by Evgeny Novikov over 3 years ago
- 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.
Updated by Evgeny Novikov over 3 years ago
- Status changed from Open to Resolved
Multiple notes per one violation witness edge (error trace node) were supported in branch extended-witnesses.
Updated by Evgeny Novikov over 3 years ago
- Status changed from Resolved to Closed
Tests passed, so, I merged the branch to master in d74545524.