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 2 years ago. Updated 9 months ago.

Status:
New
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 2 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 1 year ago

  • Category changed from Tasks generation to Results processing
#3

Updated by Evgeny Novikov over 1 year ago

I think that this is already so in master.

#4

Updated by Evgeny Novikov over 1 year ago

  • Parent task set to #8494
#5

Updated by Evgeny Novikov over 1 year ago

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

Updated by Evgeny Novikov 9 months ago

  • Target version changed from 2.0 to 3.0

Change the target version as of the parent issue.

Also available in: Atom PDF