Klever

Recent changes in witnesses processing code can result in the following "nice" exception:

WARNING> Cannot determine file for edge: '178: ldv_main_3((void *)0);'
    exec(compile(contents+"\n", file, 'exec'), glob, loc)
  File "/home/novikov/work/klever/core/core/vrp/et/__init__.py", line 60, in <module>
    et = import_error_trace(gl_logger, 'witness.0.graphml')
  File "/home/novikov/work/klever/core/core/vrp/et/__init__.py", line 25, in import_error_trace
    po = ErrorTraceParser(logger, witness)
  File "/home/novikov/work/klever/core/core/vrp/et/parser.py", line 31, in __init__
    self._check_given_files()
  File "/home/novikov/work/klever/core/core/vrp/et/parser.py", line 46, in _check_given_files
    raise ValueError('sdfasd')
ValueError: sdfasd

that can be a consequence of some edges don't have attribute "originfile". But this can happen because of for such edges a default value for that attribute should be taken. (Un)fortunately CPAchecker BAM doesn't follow this rule. It adds attribute holding file references for all edges except when they are the same for consequent edges (in that case this attribute is added just for a such first edge). Most likely we will follow this rule when we will have our own witnesses printer.

One more issue regarding CPAchecker SMG witnesses is that it started to miss global variable declaration that results in such the error during visualization:

Traceback (most recent call last):
  File "/home/novikov/work/klever/bridge/reports/views.py", line 410, in report_unsafe
    etv = GetETV(ArchiveFileContent(report, 'error_trace', ERROR_TRACE_FILE).content.decode('utf8'), request.user)
  File "/home/novikov/work/klever/bridge/reports/etv.py", line 489, in __init__
    self.html_trace, self.assumes = self.__html_trace()
  File "/home/novikov/work/klever/bridge/reports/etv.py", line 502, in __html_trace
    return self.__add_thread_lines(0, 0)[0:2]
  File "/home/novikov/work/klever/bridge/reports/etv.py", line 520, in __add_thread_lines
    parsed_trace.add_line(edge_data)
  File "/home/novikov/work/klever/bridge/reports/etv.py", line 209, in add_line
    raise ValueError("Global initialization edge can't contain enter")
ValueError: Global initialization edge can't contain enter