Klever

Bug #8192

Updated by Vitaly Mordan almost 7 years ago

The following exception occurs if may occur during error trace to be processed is empty: processing: 

 <pre> 
 <code> 
 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' 
 </code> 
 </pre> 

 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. 

 Currently 2 potential bugs were lost due to this error.

Back