Update CPAchecker SMG after it will print witnesses like CPAchecker BAM
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
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.