Project

General

Profile

Actions

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 about 4 years ago.

Status:
Closed
Priority:
Urgent
Category:
Results processing
Target version:
Start date:
01/25/2019
Due date:
% Done:

0%

Estimated time:
Published in build:

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.


Related issues 1 (0 open1 closed)

Related to Klever - Feature #9458: Visualize a new format of error tracesClosedVladimir Gratinskiy01/25/201907/02/2019

Actions
Actions #1

Updated by Evgeny Novikov about 5 years ago

  • Status changed from New to Resolved

Except for minor issues this is done in branch klever-3.0.

Actions #2

Updated by Evgeny Novikov almost 5 years ago

  • Status changed from Resolved to Closed

In master.

Actions #3

Updated by Evgeny Novikov about 4 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.

Actions #4

Updated by Evgeny Novikov about 4 years ago

  • Related to Feature #9458: Visualize a new format of error traces added
Actions #5

Updated by Evgeny Novikov about 4 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.

Actions #6

Updated by Evgeny Novikov about 4 years ago

  • Status changed from Open to Resolved

Multiple notes per one violation witness edge (error trace node) were supported in branch extended-witnesses.

Actions #7

Updated by Evgeny Novikov about 4 years ago

  • Status changed from Resolved to Closed

Tests passed, so, I merged the branch to master in d74545524.

Actions

Also available in: Atom PDF