Project

General

Profile

Bug #8485

Updated by Evgeny Novikov over 6 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. 

Back