def _translate_stm(self, oprnd1, oprnd2, oprnd3):
        assert oprnd1.size and oprnd3.size
        assert oprnd3.size == self._address_size

        op1_var = self._translate_src_oprnd(oprnd1)
        op3_var = self._translate_src_oprnd(oprnd3)

        where = op3_var
        size = oprnd1.size

        for i in xrange(0, size, 8):
            self._mem[where + i/8] = smtlibv2.EXTRACT(op1_var, i, 8)

        # Memory versioning.
        self._mem_instance += 1

        mem_old = self._mem
        mem_new = self._solver.mkArray(self._address_size, "MEM_" + str(self._mem_instance))

        self._mem = mem_new

        return [mem_new == mem_old]
Return a formula representation of a STM instruction.
dataset/ETHPy150Open programa-stic/barf-project/barf/barf/core/smt/smttranslator.py/SmtTranslator._translate_stm