		Search-engine friendly clone of the ACL2 documentation.

X86-syscall-args-and-return-value-marshalling

X86-syscall-lstat

Signature
(x86-syscall-lstat x86) → x86
Returns: x86 — Type (x86p x86), given the guard.

Definitions and Theorems

Function: x86-syscall-lstat

(defun x86-syscall-lstat (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'x86-syscall-lstat))
    (declare (ignorable __function__))
    (b* ((ctx 'x86-syscall-lstat)
         (path (rgfi *rdi* x86))
         (statbuf (rgfi *rsi* x86))
         ((when (not (canonical-address-p path)))
          (!ms (list ctx
                     :syscall-lstat-path-ptr-not-canonical)
               x86))
         ((mv flg pathname x86)
          (read-string-zero-terminated path x86))
         ((when flg)
          (!ms (list ctx :path flg) x86))
         ((mv ret x86)
          (syscall-lstat pathname statbuf x86))
         ((when (or (ms x86) (not (i64p ret))))
          (!ms (list ctx
                     :oracle-val-for-syscall-lstat ret)
               x86))
         (x86 (!rgfi *rax* ret x86)))
      x86)))

Theorem: x86p-of-x86-syscall-lstat

(defthm x86p-of-x86-syscall-lstat
  (implies (and (x86p x86))
           (b* ((x86 (x86-syscall-lstat x86)))
             (x86p x86)))
  :rule-classes :rewrite)