Project

General

Profile

Feature #8494

Process extended format of violation witnesses

Added by Evgeny Novikov about 2 years ago. Updated about 2 months ago.

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

20%

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

Bug #8196: Set the last provided with a line directory file instead of setting a default one at witness visualizationNewIlja Zakharov

Actions
Feature #9458: Visualize a new format of error tracesResolvedVladimir Gratinskiy

Actions
Feature #9459: Generate error traces in a new formatResolvedEvgeny Novikov

Actions
Feature #9824: Get rid of auxiliary functions and their removingNewEvgeny Novikov

Actions
Feature #9825: Get rid of temporary variables and their removingNewEvgeny Novikov

Actions

Related issues

Blocks Klever - Bug #8500: Environment model simplifications can break error tracesNew10/13/2017

Actions
Blocks Klever - Bug #9393: Problem with memleak visualization on absent return from void functionNew11/20/2018

Actions
Blocks Klever - Feature #9897: Develop tutorialNew10/30/2019

Actions

History

#1

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

#2

Updated by Evgeny Novikov 10 months ago

  • Assignee changed from Ilja Zakharov to Evgeny Novikov

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

#3

Updated by Evgeny Novikov about 2 months ago

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

Updated by Evgeny Novikov 14 days ago

Also available in: Atom PDF