Project

General

Profile

Bug #7938

VTG/ET failed remove return edge before violation node on parse SMG witness

Added by Anton Vasilyev about 3 years ago. Updated about 3 years ago.

Status:
Closed
Priority:
Immediate
Category:
Tasks generation
Target version:
-
Start date:
02/01/2017
Due date:
% Done:

0%

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

Description

http://ldvstore:8998/reports/unknown/77754/

Raise exception: Traceback (most recent call last): File "/home/debian/klever/core/core/components.py", line 116, in run self.main() File "/home/debian/klever/core/core/utils.py", line 56, in callbacks_caller ret = attr(*args, **kwargs) File "/home/debian/klever/core/core/vtg/rsb.py", line 44, in generate_verification_tasks self.decide_verification_task() File "/home/debian/klever/core/core/utils.py", line 56, in callbacks_caller ret = attr(*args, **kwargs) File "/home/debian/klever/core/core/vtg/rsb.py", line 316, in decide_verification_task self.process_single_verdict(decision_results, verification_report_id) File "/home/debian/klever/core/core/utils.py", line 56, in callbacks_caller ret = attr(*args, **kwargs) File "/home/debian/klever/core/core/vtg/rsb.py", line 379, in process_single_verdict et = import_error_trace(self.logger, witnesses0) File "/home/debian/klever/core/core/vtg/et/__init__.py", line 32, in import_error_trace generic_simplifications(logger, trace) File "/home/debian/klever/core/core/vtg/et/tmpvars.py", line 22, in generic_simplifications _basic_simplification(logger, trace) File "/home/debian/klever/core/core/vtg/et/tmpvars.py", line 33, in _basic_simplification error_trace.remove_edge_and_target_node(edge) File "/home/debian/klever/core/core/vtg/et/error_trace.py", line 211, in remove_edge_and_target_node raise ValueError('Is not allowed to delete violation nodes') ValueError: Is not allowed to delete violation nodes


Files

witness.0.graphml (78.6 KB) witness.0.graphml Anton Vasilyev, 02/01/2017 01:28 PM

History

#1

Updated by Evgeny Novikov about 3 years ago

  • Category set to Tasks generation
  • Priority changed from Normal to Immediate
#2

Updated by Evgeny Novikov about 3 years ago

  • Status changed from New to Resolved

Fixed in d9221e0 of fix-witness-processing.

#3

Updated by Evgeny Novikov about 3 years ago

  • Status changed from Resolved to Closed

To simplify some sort of testing I merged the branch to master in b577675.

Also available in: Atom PDF