#NEWLINE# def _translate_str( self , oprnd1 , oprnd2 , oprnd3 ) : #NEWLINE# #INDENT# 'Return a formula representation of a STR instruction.\n        ' #NEWLINE# assert ( oprnd1 . size and oprnd3 . size ) #NEWLINE# op1_var = self . _translate_src_oprnd ( oprnd1 ) #NEWLINE# ( op3_var , parent_reg_constrs ) = self . _translate_dst_oprnd ( oprnd3 ) #NEWLINE# dst_size = op3_var . size #NEWLINE# constrs = [ ] #NEWLINE# if ( oprnd1 . size == oprnd3 . size ) : #NEWLINE# #INDENT# expr = ( op1_var == op3_var ) #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# if ( oprnd1 . size < oprnd3 . size ) : #NEWLINE# #INDENT# expr = ( op1_var == smtlibv2 . EXTRACT ( op3_var , 0 , op1_var . size ) ) #NEWLINE# fmt = '#b%0{0}d' . format ( ( op3_var . size - op1_var . size ) ) #NEWLINE# imm = smtlibv2 . BitVec ( ( op3_var . size - op1_var . size ) , ( fmt % 0 ) ) #NEWLINE# constrs = [ ( imm == smtlibv2 . EXTRACT ( op3_var , op1_var . size , ( op3_var . size - op1_var . size ) ) ) ] #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# expr = ( smtlibv2 . EXTRACT ( op1_var , 0 , op3_var . size ) == op3_var ) #NEWLINE# #UNINDENT# #UNINDENT# rv = [ expr ] #NEWLINE# if constrs : #NEWLINE# #INDENT# rv += constrs #NEWLINE# #UNINDENT# if parent_reg_constrs : #NEWLINE# #INDENT# rv += parent_reg_constrs #NEWLINE# #UNINDENT# return rv