Unsafe-!undef
- Signature
(unsafe-!undef v x86) → x86
- Returns
- x86 — Type (x86p x86), given (x86p x86).
Note that unsafe-!undef is enabled, not untouchable,
and non-executable. It can be used in proof attempts but not during
execution.
unsafe-!undef should be used judiciously because updating the
undef field with a value it held previously might contaminate
our 'pool of undefined values', i.e., undef-read might then
produce a call of create-undef that collides with a previous
call of create-undef, which would make the result of an
equality test between them equal instead of indeterminate.
An example of an acceptable use of unsafe-!undef is to
specify the undef field in a final x86 state during a proof
attempt.
Definitions and Theorems
Function: unsafe-!undef
(defun unsafe-!undef (v x86)
(declare (xargs :stobjs (x86)))
(declare (xargs :non-executable t))
(declare (xargs :guard t))
(prog2$ (acl2::throw-nonexec-error 'unsafe-!undef
(list v x86))
(let ((__function__ 'unsafe-!undef))
(declare (ignorable __function__))
(!undef v x86))))
Theorem: x86p-of-unsafe-!undef
(defthm x86p-of-unsafe-!undef
(implies (x86p x86)
(b* ((x86 (unsafe-!undef v x86)))
(x86p x86)))
:rule-classes :rewrite)
