		Search-engine friendly clone of the ACL2 documentation.

Defabsstobj

Illegal-state

Illegal ACL2 state

See set-absstobj-debug for background on invariance violations for abstract stobjs. In short, they may occur when execution does not complete for certain atomic operations.

Such violations cause the following error message to be printed.

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.

At this point, the only way to get ACL2 to evaluate further input is to submit the form :CONTINUE-FROM-ILLEGAL-STATE, as noted above — or more generally, the form it actually represents, (CONTINUE-FROM-ILLEGAL-STATE), which may need to be written as (ACL2::CONTINUE-FROM-ILLEGAL-STATE) if the current-package is other than "ACL2". There is actually one exception: :q is accepted, to pop out of the current call of ld.

To get a bit more information from the error message displayed above, see set-absstobj-debug.

See community-book file books/system/tests/abstract-stobj-nesting/nested-abstract-stobjs-input.lsp, Examples 3 and 4, for relevant examples.

Technical note. An illegal-state is entered when ACL2 sets the ld special, ld-pre-eval-print, to the value :illegal-state.