Project

General

Profile

Bug #8500

Environment model simplifications can break error traces

Added by Evgeny Novikov over 2 years ago. Updated 5 months ago.

Status:
Rejected
Priority:
Urgent
Assignee:
-
Category:
Results processing
Target version:
Start date:
10/13/2017
Due date:
% Done:

0%

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

Description

For instance, when I switched off CIL merging for module "drivers/hwmon/dme1737.ko" of Linux 3.14 checked against "linux:fs:sysfs" I got the following exception:

Raise exception:
Traceback (most recent call last):
  File "/home/novikov/work/klever/core/core/components.py", line 118, in run
    self.main()
  File "/home/novikov/work/klever/core/core/utils.py", line 95, in callbacks_caller
    ret = attr(*args, **kwargs)
  File "/home/novikov/work/klever/core/core/vrp/__init__.py", line 225, in fetcher
    raise self.__exception
  File "/home/novikov/work/klever/core/core/vrp/__init__.py", line 341, in process_single_verdict
    error_trace = et.import_error_trace(self.logger, witnesses[0])
  File "/home/novikov/work/klever/core/core/vrp/et/__init__.py", line 38, in import_error_trace
    envmodel_simplifications(logger, trace)
  File "/home/novikov/work/klever/core/core/vrp/et/envmodel.py", line 27, in envmodel_simplifications
    error_trace.final_checks()
  File "/home/novikov/work/klever/core/core/vrp/et/error_trace.py", line 429, in final_checks
    self.resolve_function(data[-1])))
ValueError: Unexpected return from function '_tmp_dme1737_abs_paths_trimmed_idme1737_sio_inb' in thread 2, expected last entered function _tmp_dme1737_abs_paths_trimmed_ioutb

Similar exceptions broke processing of 28 of 35 error traces.

History

#1

Updated by Ilja Zakharov over 2 years ago

  • Assignee changed from Ilja Zakharov to Evgeny Novikov

I checked it out and saw that without our general optimizations environment model simplifications work well and the witness can be at least visualized. However, the visualization contains suspicious None lines. Evgeny, I propose first you update general optimizations and then revisit the issue.

#2

Updated by Evgeny Novikov over 2 years ago

  • Target version changed from 1.0 to 2.0

Let's consider everything related with witnesses in Klever 1.0. I hope that we will at last have a new format and a new printer of witnesses there that will be a great step forward. In particular, this issue can become irrelevant.

#3

Updated by Evgeny Novikov almost 2 years ago

  • Target version changed from 2.0 to 3.0

Change the target the version as of the blocking issue.

#4

Updated by Evgeny Novikov 5 months ago

  • Blocked by deleted (Feature #8494: Process extended format of violation witnesses)
#5

Updated by Evgeny Novikov 5 months ago

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

I suggest to reject this issue since we do not consider verification without CIL. Let's open more relevant issues if so.

Also available in: Atom PDF