(write-string-to-memory ptr str x86) → (mv flg x86)
Function:
(defun write-string-to-memory (ptr str x86) (declare (xargs :stobjs (x86))) (declare (type (signed-byte 49) ptr)) (declare (xargs :guard (and (stringp str) (integerp ptr) (<= (- *2^47*) ptr) (< (+ -1 ptr (length str)) *2^47*)) :split-types t)) (let ((__function__ 'write-string-to-memory)) (declare (ignorable __function__)) (let ((bytes (string-to-bytes str))) (write-bytes-to-memory ptr bytes x86))))
Theorem:
(defthm x86p-of-write-string-to-memory.x86 (implies (x86p x86) (b* (((mv ?flg ?x86) (write-string-to-memory ptr str x86))) (x86p x86))) :rule-classes :rewrite)