Project

General

Profile

Bug #8196

Feature #8494: Process extended format of violation witnesses

Set the last provided with a line directory file instead of setting a default one at witness visualization

Added by Ilja Zakharov about 3 years ago. Updated 5 months ago.

Status:
Rejected
Priority:
Urgent
Assignee:
-
Category:
Results processing
Target version:
Start date:
05/11/2017
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

Since a cil file can contain lines with only line numbers or even lines without line directives at all our witness trace processor should correctly process witnesses for such files. I observe the following issues currently:
  1. If a line directive is given without a file our witness processor should add the last referred file but not any default one.
  2. If for a line there is no line directive such lines should be somehow hidden or processed differently since startline data tag refers in the case to cilled file instead of an original C file.

The last issue hardly can be fixed without changing witness format.

History

#1

Updated by Evgeny Novikov almost 3 years ago

Ilja Zakharov wrote:

Since a cil file can contain lines with only line numbers or even lines without line directives at all our witness trace processor should correctly process witnesses for such files. I observe the following issues currently:
  1. If a line directive is given without a file our witness processor should add the last referred file but not any default one.

This is likely a bug in verification tool. As far as I understand default values should be used if no values are specified in accordance with the GraphML format.

  1. If for a line there is no line directive such lines should be somehow hidden or processed differently since startline data tag refers in the case to cilled file instead of an original C file.

This also seems to be a bug in verification tool. There is a common assumption that if processed line numbers correspond original ones then line directives aren't printed.

#2

Updated by Evgeny Novikov over 2 years ago

  • Category changed from Tasks generation to Results processing
#3

Updated by Evgeny Novikov over 2 years ago

I think that this is already so in master.

#4

Updated by Evgeny Novikov over 2 years ago

  • Parent task set to #8494
#5

Updated by Evgeny Novikov over 2 years ago

  • Assignee set to Ilja Zakharov
  • Priority changed from High to Urgent
  • Target version set to 2.0
#6

Updated by Evgeny Novikov almost 2 years ago

  • Target version changed from 2.0 to 3.0

Change the target version as of the parent issue.

#7

Updated by Evgeny Novikov 6 months ago

  • Assignee changed from Ilja Zakharov to Evgeny Novikov

I will take care about this.

#8

Updated by Evgeny Novikov 5 months ago

  • Assignee deleted (Evgeny Novikov)
  • Status changed from New to Rejected

I think that this issue is not relevant anymore since we changed the whole approach to refer to original source files.

Also available in: Atom PDF