Project

General

Profile

Actions
Copy link

Feature #8494

closed

Process extended format of violation witnesses

Added by Evgeny Novikov over 6 years ago. Updated over 3 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Evgeny Novikov
Category:
Results processing
Target version:
3.0
Start date:
05/11/2017
Due date:
07/02/2019
% Done:

100%

Estimated time:
(Total: 0.00 h)
Published in build:

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.

Subtasks 5 (0 open — 5 closed)

Bug #8196: Set the last provided with a line directory file instead of setting a default one at witness visualizationRejected05/11/2017

Actions
Feature #9458: Visualize a new format of error tracesClosedVladimir Gratinskiy01/25/201907/02/2019

Actions
Feature #9459: Generate error traces in a new formatClosedEvgeny Novikov01/25/2019

Actions
Feature #9824: Get rid of auxiliary functions and their removingClosedEvgeny Novikov09/18/2019

Actions
Feature #9825: Get rid of temporary variables and their removingClosedEvgeny Novikov09/18/2019

Actions

Related issues 2 (0 open — 2 closed)

Blocked by Klever - Feature #10043: Update CPAcheckerClosedEvgeny Novikov01/17/2020

Actions
Blocks Klever - Feature #10465: Update Klever tutorialClosedEvgeny Novikov08/17/2020

Actions
Actions
Copy link
 #1

Updated by Evgeny Novikov over 5 years ago

  • 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.

Actions
Copy link
 #2

Updated by Evgeny Novikov about 5 years ago

  • Assignee changed from Ilja Zakharov to Evgeny Novikov

Ilja will do a real job unlike us in near future.

Actions
Copy link
 #3

Updated by Evgeny Novikov over 4 years ago

  • Blocks Bug #9393: Problem with memleak visualization on absent return from void function added
Actions
Copy link
 #4

Updated by Evgeny Novikov over 4 years ago

Actions
Copy link
 #5

Updated by Evgeny Novikov about 4 years ago

  • Blocks deleted (Bug #8500: Environment model simplifications can break error traces)
Actions
Copy link
 #6

Updated by Evgeny Novikov about 4 years ago

  • Blocks deleted (Bug #9393: Problem with memleak visualization on absent return from void function)
Actions
Copy link
 #7

Updated by Evgeny Novikov about 4 years ago

Actions
Copy link
 #8

Updated by Evgeny Novikov almost 4 years ago

Actions
Copy link
 #9

Updated by Evgeny Novikov over 3 years ago

Actions
Copy link
 #10

Updated by Evgeny Novikov over 3 years ago

Actions
Copy link
 #11

Updated by Evgeny Novikov over 3 years ago

Actions
Copy link
 #12

Updated by Evgeny Novikov over 3 years ago

  • 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.

Actions
Copy link

Also available in: Atom PDF