#NEWLINE# def parse_XML( self , output , returncode , isTimeout ) : #NEWLINE# #INDENT# def sanitizeXML( s ) : #NEWLINE# #INDENT# return s . replace ( '<>' , '<emptyTag>' ) . replace ( '</>' , '</emptyTag>' ) #NEWLINE# #UNINDENT# try : #NEWLINE# #INDENT# tree = ET . fromstringlist ( map ( sanitizeXML , output ) ) #NEWLINE# status = tree . findtext ( 'cprover-status' ) #NEWLINE# if ( status is None ) : #NEWLINE# #INDENT# def isErrorMessage( msg ) : #NEWLINE# #INDENT# return ( msg . get ( 'type' , None ) == 'ERROR' ) #NEWLINE# #UNINDENT# messages = list ( filter ( isErrorMessage , tree . getiterator ( 'message' ) ) ) #NEWLINE# if messages : #NEWLINE# #INDENT# msg = messages [ 0 ] . findtext ( 'text' ) #NEWLINE# if ( msg == 'Out of memory' ) : #NEWLINE# #INDENT# status = 'OUT OF MEMORY' #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# if msg : #NEWLINE# #INDENT# status = 'ERROR ({0})' . format ( msg ) #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# status = 'ERROR' #NEWLINE# #UNINDENT# #UNINDENT# #UNINDENT# else : #NEWLINE# #INDENT# status = 'INVALID OUTPUT' #NEWLINE# #UNINDENT# #UNINDENT# else : #NEWLINE# #INDENT# if ( status == 'FAILURE' ) : #NEWLINE# #INDENT# assert ( returncode == 10 ) #NEWLINE# reason = tree . find ( 'goto_trace' ) . find ( 'failure' ) . findtext ( 'reason' ) #NEWLINE# if ( not reason ) : #NEWLINE# #INDENT# reason = tree . find ( 'goto_trace' ) . find ( 'failure' ) . get ( 'reason' ) #NEWLINE# #UNINDENT# if ( 'unwinding assertion' in reason ) : #NEWLINE# #INDENT# status = result . RESULT_UNKNOWN #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# status = result . RESULT_FALSE_REACH #NEWLINE# #UNINDENT# #UNINDENT# else : #NEWLINE# #INDENT# if ( status == 'SUCCESS' ) : #NEWLINE# #INDENT# assert ( returncode == 0 ) #NEWLINE# if ( '--no-unwinding-assertions' in self . options ) : #NEWLINE# #INDENT# status = result . RESULT_UNKNOWN #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# status = result . RESULT_TRUE_PROP #NEWLINE# #UNINDENT# #UNINDENT# #UNINDENT# #UNINDENT# #UNINDENT# except Exception : #NEWLINE# #INDENT# if tree : #NEWLINE# #INDENT# status = 'TIMEOUT' #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# if ( 'Minisat::OutOfMemoryException' in output ) : #NEWLINE# #INDENT# status = 'OUT OF MEMORY' #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# status = 'INVALID OUTPUT' #NEWLINE# logging . exception ( 'Error parsing CBMC output for returncode %d' , returncode ) #NEWLINE# #UNINDENT# #UNINDENT# #UNINDENT# return status