Project

General

Profile

Actions

Bug #7992

closed

RSB fails at witnesses processing during validation run

Added by Ilja Zakharov about 7 years ago. Updated about 7 years ago.

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

0%

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

Description

Currently there are 5 unsafes cannot be visualized after the run of the validation set (d8e172f3c0a5, 448356262f56~, 214c97a12f1f, c822fb57ba12, c822fb57ba12~) due to error at RSB:

Traceback (most recent call last):
File "/work/zakharov/src/klever/core/core/components.py", line 116, in run
self.main()
File "/work/zakharov/src/klever/core/core/utils.py", line 56, in callbacks_caller
ret = attr(*args, **kwargs)
File "/work/zakharov/src/klever/core/core/vtg/rsb.py", line 46, in generate_verification_tasks
self.decide_verification_task()
File "/work/zakharov/src/klever/core/core/utils.py", line 56, in callbacks_caller
ret = attr(*args, **kwargs)
File "/work/zakharov/src/klever/core/core/vtg/rsb.py", line 318, in decide_verification_task
self.process_single_verdict(decision_results, verification_report_id)
File "/work/zakharov/src/klever/core/core/utils.py", line 56, in callbacks_caller
ret = attr(*args, **kwargs)
File "/work/zakharov/src/klever/core/core/vtg/rsb.py", line 409, in process_single_verdict
et = import_error_trace(self.logger, witnesses0)
File "/work/zakharov/src/klever/core/core/vtg/et/__init__.py", line 32, in import_error_trace
generic_simplifications(logger, trace)
File "/work/zakharov/src/klever/core/core/vtg/et/tmpvars.py", line 25, in generic_simplifications
_remove_aux_functions(logger, trace)
File "/work/zakharov/src/klever/core/core/vtg/et/tmpvars.py", line 287, in _remove_aux_functions
actual_args[i] = aux_actual_args[j]
IndexError: list index out of range

Actions #1

Updated by Evgeny Novikov about 7 years ago

  • Status changed from New to Closed

I fixed this in a47d838 to master. So now all 5 mentioned unsafes can be pretty found.

Actions

Also available in: Atom PDF