		Search-engine friendly clone of the ACL2 documentation.

Virtualization-for-validation

Validate-inst

Handles a single back and forth with the C program over the socket. Smashed in raw lisp.

Signature
(validate-inst x86) → (mv * x86)

Definitions and Theorems

Function: validate-inst

(defun validate-inst (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'validate-inst))
    (declare (ignorable __function__))
    (mv nil x86)))