Get more information when atomic update fails for an abstract stobj
This documentation topic assumes familiarity with abstract stobjs. See defabsstobj.
Below we explain what is meant by the following error message, and how to add information to the end of it.
ACL2 Error in CHK-ABSSTOBJ-INVARIANTS: Possible invariance violation for an abstract stobj! **PROCEED AT YOUR OWN RISK.** To proceed, evaluate the following form. :CONTINUE-FROM-ILLEGAL-STATE See :DOC set-absstobj-debug.
Advanced users who are willing to risk unsound invariance violations to get a bit more speed may submit the following when there is an active trust tag (see defttag).
The rest of the session will then avoid the error message above because it
avoids the abstract stobj invariance checking discussed belowq. BUT WITHOUT
THIS CHECKING, YOUR SESSION COULD BE CORRUPTED! The discussion below assumes
that you are not using the special argument
The use of
ACL2 Error in CHK-ABSSTOBJ-INVARIANTS: Possible invariance violation for an abstract stobj! **PROCEED AT YOUR OWN RISK.** To proceed, evaluate the following form. :CONTINUE-FROM-ILLEGAL-STATE See :DOC set-absstobj-debug. Evaluation was aborted under a call of abstract stobj export UPDATE-FLD-NIL-BAD.
You may be best off starting a new ACL2 session if you see one of the
errors above. But you can continue at your own risk. With a trust tag (see
defttag), you can even fool ACL2 into thinking nothing is wrong, and
perhaps you can fix up the abstract stobj so that indeed, nothing really is
wrong. See the community-books file
Examples: (set-absstobj-debug t) ; obtain extra debug info, as above (set-absstobj-debug nil) ; avoid extra debug info (default) (set-absstobj-debug :ignore) ; possibly unsound! -- see above General Form: (set-absstobj-debug val)
Recall (see defabsstobj) that for any exported function whose