Bug #8485
Updated by Evgeny Novikov about 7 years ago
Recent changes in witnesses processing code can result in the following "nice" exception:
<pre>
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
</pre>
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
This 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:
<pre>
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
</pre> regression issue.