Bug #8192
closedException during empty error trace processing
0%
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
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.
Updated by Vitaly Mordan almost 7 years ago
- File witness.12.graphml witness.12.graphml added
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.
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)
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.
Updated by Evgeny Novikov over 6 years ago
- Category changed from Tasks generation to Results processing
Updated by Evgeny Novikov about 3 years ago
- Status changed from Open to Rejected
I don't believe that the issue exists still.