Project

General

Profile

Actions
Copy link

Bug #7927

closed

VTG/ET throws exception on parse SMG witness

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

Status:
Rejected
Priority:
Normal
Assignee:
-
Category:
-
Target version:
-
Start date:
01/30/2017
Due date:
% Done:

0%

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

Description

http://ldvstore:8998/reports/unknown/73959/

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 317, 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 380, 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 209, in remove_edge_and_target_node raise ValueError('Cannot delete edge with warning: {!r}'.format(edge['source'])) KeyError: 'source'

Files

witness.0.graphml (63.8 KB) witness.0.graphml Anton Vasilyev, 01/30/2017 05:18 PM
Actions
Copy link
 #1

Updated by Anton Vasilyev about 7 years ago

Probably fix should be done at SMGCPA

Actions
Copy link
 #2

Updated by Evgeny Novikov about 7 years ago

  • Category deleted (Bridge)
  • Status changed from New to Rejected
  • Assignee deleted (Evgeny Novikov)

Anton identified that this issue is due to SMGCPA provides edges that have warnings but don't have attribute sourcecode. Klever always removes such the edges by default since it can't perform many useful transformations and nice visualization for such edges, but removing edges with warnings can't be considered good at all.

Actions
Copy link

Also available in: Atom PDF