Feature #8494
closed
Process extended format of violation witnesses
Added by Evgeny Novikov over 6 years ago.
Updated over 3 years ago.
Category:
Results processing
Estimated time:
(Total: 0.00 h)
Description
We already had a lot of issues regarding various printers of violation witnesses. And we will have them unless there will be the only printer of witnesses that will follow the extended format. Moreover, the new approach will allow to avoid changes with printing of violation witnesses in any static verification tools. Each of them will either strictly follow the extended format itself or their witnesses will be passed through the printer.
- Target version changed from 2.0 to 3.0
I don't believe that we will be able to include this into Klever 2.0.
- Assignee changed from Ilja Zakharov to Evgeny Novikov
Ilja will do a real job unlike us in near future.
- Blocks Bug #9393: Problem with memleak visualization on absent return from void function added
- Blocks deleted (Bug #8500: Environment model simplifications can break error traces)
- Blocks deleted (Bug #9393: Problem with memleak visualization on absent return from void function)
- Status changed from New to Closed
At last all subtasks are closed, so, we have support for extended violation witnesses in master! This change is not backward compatible, so, you need to re-install Klever completely after update. I hope that this is the last such change for Klever 3.0 and much time beyond.
Also available in: Atom
PDF