You may see a warning like this:
ACL2 Warning [Invariant-risk] in MY-FUNCTION: Invariant-risk has been detected for a call of function MY-FUNCTION (as possibly leading to an ill-guarded call of UPDATE-FLD); see :DOC invariant-risk.
Such warnings indicate potential slowdown due to aggressive protection by ACL2 against either:
(defstobj st (fld :type integer :initially 0)) (defun f (n st) (declare (xargs :stobjs st :guard (integerp n))) (update-fld n st)) ; This :program-mode wrapper for f fails to require (integerp n): (defun g (n st) (declare (xargs :stobjs st :mode :program)) (f n st)) ; Produces an invariant-risk warning: (g 3 st) ; Produces an invariant-risk warning and a guard violation: (g 'a st)
Each of the two calls of
We may say that such
There are two general methods for avoiding such warnings: at runtime with
set-check-invariant-risk, and at definition time with set-register-invariant-risk. We describe each briefly below. For more
information follow the links just above to their respective documentation
topics. For yet more detail about invariant-risk see invariant-risk-details. For tools that may help find sources of
invariant-risk, see community-book
You can avoid seeing warnings like the one displayed above (without affecting the check that is actually performed) by evaluating either one of the following forms.
(set-check-invariant-risk t) (set-inhibit-warnings "invariant-risk")
You can also replace such warnings by errors:
On occasion you may define functions that you know avoid invariant-risk danger, even though ACL2 designates those functions as having invariant-risk. Rather than removing invariant-risk checking for all functions at runtime with set-check-invariant-risk, it is probably much safer to remove it only for the functions in a given book or encapsulate event. See set-register-invariant-risk for how to do that.