Bug #8485

Update CPAchecker SMG after it will print witnesses like CPAchecker BAM

Added by Evgeny Novikov almost 3 years ago. Updated almost 3 years ago.

Results processing
Target version:
Start date:
Due date:
% Done:


Estimated time:
Detected in build:
Published in build:


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/", line 60, in <module>
    et = import_error_trace(gl_logger, 'witness.0.graphml')
  File "/home/novikov/work/klever/core/core/vrp/et/", line 25, in import_error_trace
    po = ErrorTraceParser(logger, witness)
  File "/home/novikov/work/klever/core/core/vrp/et/", line 31, in __init__
  File "/home/novikov/work/klever/core/core/vrp/et/", 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/", 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/", line 489, in __init__
    self.html_trace, self.assumes = self.__html_trace()
  File "/home/novikov/work/klever/bridge/reports/", line 502, in __html_trace
    return self.__add_thread_lines(0, 0)[0:2]
  File "/home/novikov/work/klever/bridge/reports/", line 520, in __add_thread_lines
  File "/home/novikov/work/klever/bridge/reports/", line 209, in add_line
    raise ValueError("Global initialization edge can't contain enter")
ValueError: Global initialization edge can't contain enter



Updated by Evgeny Novikov almost 3 years ago

  • Subject changed from Respect default value for witness attribute "originfile" to Update CPAchecker SMG after it will print witnesses like CPAchecker BAM
  • Description updated (diff)

Updated by Ilja Zakharov almost 3 years ago

The exception is horrible but the issue is relatively strong connected with #8196. Since all three CPAchecker versions and Ultimate differently use the default file and an entry point indication it is extremely difficult to propose a universal working solution.


Updated by Evgeny Novikov almost 3 years ago

  • Status changed from New to Closed

I did this in 06176303. But I still can't visualize error trace for the only unsafe test for generic:memory due to #8496.

Also available in: Atom PDF