|
|
|---|
|
|
|
|---|
A mode that avoids guard violations on primitives
ACL2 has a special mode, called ``safe mode'', that guarantees that built-in ACL2 primitives check their guards even even when set-guard-checking has turned off guard-checking. This mode is used for macroexpansion as well as in processing a few other kinds of forms, notably defconst, defpkg, and value-triple events.
Use of this mode avoids the possibility of certain errors when loading a compiled file for a book. Consider the following definitions.
(defun foo (x) (declare (xargs :guard (consp x))) (car x)) (defmacro bar () (foo 3))
Then we can see
ACL2 !>(set-guard-checking nil) Masking guard violations but still checking guards except for self- recursive calls. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard-checking. ACL2 >(bar) ACL2 Error in TOP-LEVEL: In the attempt to macroexpand the form (BAR), evaluation of the macro body caused the following error: The guard for the function call (CAR X), which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (CAR 3). The guard is being checked because this function is a primitive and a "safe" mode is being used for defconst, defpkg, macroexpansion, or another operation where safe mode is required. To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 >
Notice that because of the
To understand how safe-mode works we refer to the notion of
``executable-counterpart''; see evaluation for relevant background.
ACL2 arranges for that for the executable-counterpart of any program mode
function,