		Search-engine friendly clone of the ACL2 documentation.

Characterizing-undefined-behavior

Undef-read

Get a unique unknown to be used when reasoning about undefined values in the processor

Signature
(undef-read x86) → (mv unknown x86)
Returns: unknown — Type (natp unknown).; x86 — Type (x86p x86), given (x86p x86).

See characterizing-undefined-behavior for more details.

The accessor and updater functions of the undef field are untouchable so that the only way to create a new seed for unknowns is via this function.

Definitions and Theorems

Function: undef-read$notinline

(defun undef-read$notinline (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'undef-read))
    (declare (ignorable __function__))
    (undef-read-logic x86)))

Theorem: natp-of-undef-read.unknown

(defthm natp-of-undef-read.unknown
  (b* (((mv ?unknown ?x86)
        (undef-read$notinline x86)))
    (natp unknown))
  :rule-classes :type-prescription)

Theorem: x86p-of-undef-read.x86

(defthm x86p-of-undef-read.x86
  (implies (x86p x86)
           (b* (((mv ?unknown ?x86)
                 (undef-read$notinline x86)))
             (x86p x86)))
  :rule-classes :rewrite)

Subtopics

Unsafe-!undef
Undef-read-logic