Project

General

Profile

Actions

Bug #8192

closed

Exception during empty error trace processing

Added by Vitaly Mordan almost 7 years ago. Updated about 3 years ago.

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

0%

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

Description

The following exception occurs if error trace to be processed is empty:


Raise exception:
Traceback (most recent call last):
  File "/home/ubuntu/klever/core/core/components.py", line 116, in run
    self.main()
  File "/home/ubuntu/klever/core/core/utils.py", line 56, in callbacks_caller
    ret = attr(*args, **kwargs)
  File "/home/ubuntu/klever/core/core/vtg/rsb.py", line 46, in generate_verification_tasks
    self.decide_verification_task()
  File "/home/ubuntu/klever/core/core/utils.py", line 56, in callbacks_caller
    ret = attr(*args, **kwargs)
  File "/home/ubuntu/klever/core/core/vtg/rsb.py", line 322, in decide_verification_task
    raise self.witness_processing_exception
  File "/home/ubuntu/klever/core/core/vtg/rsb.py", line 426, in process_single_verdict
    et = import_error_trace(self.logger, witnesses[0])
  File "/home/ubuntu/klever/core/core/vtg/et/__init__.py", line 25, in import_error_trace
    po = ErrorTraceParser(logger, witness)
  File "/home/ubuntu/klever/core/core/vtg/et/parser.py", line 31, in __init__
    self._parse_witness(witness)
  File "/home/ubuntu/klever/core/core/vtg/et/parser.py", line 48, in _parse_witness
    sink_nodes_map = self.__parse_witness_nodes(graph)
  File "/home/ubuntu/klever/core/core/vtg/et/parser.py", line 84, in __parse_witness_nodes
    if not self.error_trace.entry_node:
  File "/home/ubuntu/klever/core/core/vtg/et/error_trace.py", line 56, in entry_node
    return self._nodes[self._entry_node_id]
KeyError: 'A236192'

How to reproduce:
Linux kernel: 4.2.6
Klever version: master (d70964d).
CPAchecker version: ldv-bam:24643
Rule: linux:usb:dev
Module: drivers/net/wireless/at76c50x-usb.ko, drivers/mmc/host/vub300.


Files

witness.12.graphml (3.85 KB) witness.12.graphml Vitaly Mordan, 05/04/2017 05:52 PM
Actions #1

Updated by Ilja Zakharov almost 7 years ago

  • Status changed from New to Feedback

Please, attach a corresponding witness XML for the error. By the way, ensure, please, that it is correct and consistent and actually contains the node with such identifier.

Actions #3

Updated by Ilja Zakharov almost 7 years ago

  • Status changed from Feedback to Open

It is an empty witness that does not contain any edges and contains the only node which is an entry and a sink at the same time. I agree that it is a corner case for our parser that is better to fix. But it does not prevent finding any bugs since the witness does not describe anything meaningful.

Actions #4

Updated by Vitaly Mordan almost 7 years ago

  • Subject changed from Exception during error trace processing to Exception during empty error trace processing
  • Description updated (diff)
Actions #5

Updated by Evgeny Novikov almost 7 years ago

  • Category set to Tasks generation
  • Priority changed from Normal to High

This is a new bug in a new version of CPAchecker BAM. But I agree that Core shouldn't raise such the exception and should check for the expected error traces format better.

Actions #6

Updated by Evgeny Novikov over 6 years ago

  • Category changed from Tasks generation to Results processing
Actions #7

Updated by Evgeny Novikov about 3 years ago

  • Status changed from Open to Rejected

I don't believe that the issue exists still.

Actions

Also available in: Atom PDF